Merge pull request #3479 from FStarLang/guido_Prims

Moving prims.fst to Prims.fst
FStarLang · Sep 16, 2024 · 921b8c3 · 921b8c3
2 parents 0cc81be + 973e90c
commit 921b8c3
Show file tree

Hide file tree

Showing 43 changed files with 524 additions and 529 deletions.
diff --git a/.ci/fsdoc.sh b/.ci/fsdoc.sh
@@ -24,7 +24,7 @@ pushd ulib
 FST_FILES=(FStar.*.fst FStar.*.fsti)
 
 # In case some files needs to be removed use this:
-# FST_FILES=( ${FST_FILES[@]/"prims.fst"} )
+# FST_FILES=( ${FST_FILES[@]/"Prims.fst"} )
 
 ../bin/fstar-any.sh --odir "../$FSDOC_ODIR" --doc ${FST_FILES[*]} 
 popd

diff --git a/doc/book/code/Makefile b/doc/book/code/Makefile
@@ -20,7 +20,8 @@ depend: .depend
 	touch -c $@
 
 wc:
-	wc -l prims.fst $(ALL)
+	# Prims.fst seems to be missing here?
+	wc -l Prims.fst $(ALL)
 
 
 extract:

diff --git a/doc/book/code/exercises/Makefile b/doc/book/code/exercises/Makefile
@@ -17,7 +17,7 @@ depend: .depend
 	touch -c $@
 
 wc:
-	wc -l prims.fst $(ALL)
+	wc -l Prims.fst $(ALL)
 
 
 extract:

diff --git a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Base.ml b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Base.ml
diff --git a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Effectful.ml b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Effectful.ml
diff --git a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_ExploreTerm.ml b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_ExploreTerm.ml
diff --git a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Output.ml b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Output.ml