Merge pull request #3454 from mtzguido/include

src: use fstar.include

src/Makefile.boot.common

@@ -2,6 +2,7 @@
 # Makefile.boot includes it too for bootstrapping
 # Makefiles that include it should define FSTAR_HOME before the include
 
+# Used by Pulse, remove later
 INCLUDE_PATHS = \
 	basic \
 	class \
@@ -23,7 +24,7 @@ CACHE_DIR?=$(FSTAR_HOME)/src/.cache.boot
 
 # 274, else we get a warning for shadowing parse.fsi, when opening FStar.Parser namespace
 
-FSTAR_BOOT_OPTIONS=$(OTHERFLAGS) --lax --no_location_info --warn_error -271-272-241-319-274 --cache_dir $(CACHE_DIR) $(addprefix --include , $(addprefix $(FSTAR_HOME)/src/,$(INCLUDE_PATHS)))
+FSTAR_BOOT_OPTIONS=$(OTHERFLAGS) --lax --no_location_info --warn_error -271-272-241-319-274 --cache_dir $(CACHE_DIR)
 
 %.fsti-in %.fst-in:
 	@echo $(FSTAR_BOOT_OPTIONS)

src/extraction/FStar.Extraction.ML.PrintML.fst

@@ -20,6 +20,12 @@ open FStar.Compiler
 open FStar.Extraction.ML.Syntax
 open FStar.Extraction.ML.Code
 
+(* NOTE!!!! This file is not used by the OCaml build of F* (i.e. the main one).
+Instead, it uses an OCaml version ocaml/fstar-lib/FStar_Extraction_ML_PrintML,
+so it can use OCaml's native pretty printers.
+
+This file is here for the F# build. *)
+
 let print (_: option string) (ext: string) (l: mllib) =
     let newDoc = FStar.Extraction.ML.Code.doc_of_mllib l in
     List.iter (fun (n,d) ->

src/fstar.include

@@ -0,0 +1,15 @@
+basic
+class
+data
+extraction
+fstar
+parser
+prettyprint
+reflection
+smtencoding
+syntax
+syntax/print
+tactics
+tosyntax
+typechecker
+tests