Merge pull request #2342 from FStarLang/nik_remove_eta_boot

Restore BatList implementation for FStar.Compiler.List
FStarLang · Jul 28, 2021 · cf50228 · cf50228
2 parents d2d3a3d + 47f4a57
commit cf50228
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 446 deletions.
diff --git a/src/Makefile.boot b/src/Makefile.boot
@@ -37,7 +37,7 @@ EXTRACT_MODULES=FStar.Pervasives FStar.Common FStar.Compiler.Range FStar.Thunk
 # And there are a few specific files that should not be extracted at
 # all, despite being in one of the EXTRACT_NAMESPACES
 NO_EXTRACT=FStar.Tactics.Native FStar.Tactics.Load	\
-	   FStar.Extraction.ML.PrintML
+	   FStar.Extraction.ML.PrintML FStar.Compiler.List
 
 EXTRACT = $(addprefix --extract_module , $(EXTRACT_MODULES))		\
 	  $(addprefix --extract_namespace , $(EXTRACT_NAMESPACES))	\

diff --git a/src/basic/ml/FStar_Compiler_List.ml b/src/basic/ml/FStar_Compiler_List.ml
@@ -0,0 +1,3 @@
+(* We give an implementation here using OCaml's BatList,
+   which provides tail-recursive versions of most functions *)
+include FStar_List