diff --git a/.ci/fsdoc.sh b/.ci/fsdoc.sh
index feecdb76391..17eddb68d1a 100755
--- 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
index 0416dd3ae49..fa279e9e213 100644
--- 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
index 6067df3b796..9ebf84e3b93 100644
--- 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
index 96c24172482..a03dea82c49 100644
--- a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Base.ml
+++ b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Base.ml
@@ -97,7 +97,7 @@ let option_to_string :
(Prims.of_int (48)) (Prims.of_int (30)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___1)
@@ -113,7 +113,7 @@ let option_to_string :
(Prims.of_int (48)) (Prims.of_int (36)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -151,7 +151,7 @@ let list_to_string :
(Prims.of_int (58)) (Prims.of_int (52)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___3)
@@ -167,7 +167,7 @@ let list_to_string :
(Prims.of_int (58)) (Prims.of_int (59)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___2)
@@ -183,7 +183,7 @@ let list_to_string :
(Prims.of_int (58)) (Prims.of_int (59)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___1)
(fun uu___2 ->
@@ -197,7 +197,7 @@ let list_to_string :
(Prims.of_int (68)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
(fun uu___1 ->
@@ -300,7 +300,7 @@ let (abv_to_string :
(Prims.of_int (85)) (Prims.of_int (15)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___1)
(fun uu___2 ->
@@ -349,7 +349,7 @@ let (print_binder_info :
(Prims.of_int (92)) (Prims.of_int (45)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___1)
@@ -500,7 +500,7 @@ let (print_binder_info :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -529,7 +529,7 @@ let (print_binder_info :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -559,7 +559,7 @@ let (print_binder_info :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -589,7 +589,7 @@ let (print_binder_info :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -621,7 +621,7 @@ let (print_binder_info :
(
Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -649,7 +649,7 @@ let (print_binder_info :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -678,7 +678,7 @@ let (print_binder_info :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -708,7 +708,7 @@ let (print_binder_info :
(Obj.magic
(
FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -736,7 +736,7 @@ let (print_binder_info :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -761,7 +761,7 @@ let (print_binder_info :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -783,7 +783,7 @@ let (print_binder_info :
(Prims.of_int (47)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -804,7 +804,7 @@ let (print_binder_info :
(Prims.of_int (47)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -892,7 +892,7 @@ let (acomp_to_string :
(Prims.of_int (113)) (Prims.of_int (36)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___1)
(fun uu___2 ->
@@ -906,7 +906,7 @@ let (acomp_to_string :
(Prims.of_int (113)) (Prims.of_int (42)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___)
(fun uu___1 ->
@@ -923,7 +923,7 @@ let (acomp_to_string :
(Prims.of_int (115)) (Prims.of_int (37)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___1)
(fun uu___2 ->
@@ -937,7 +937,7 @@ let (acomp_to_string :
(Prims.of_int (115)) (Prims.of_int (43)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___)
(fun uu___1 ->
@@ -973,7 +973,7 @@ let (acomp_to_string :
(Prims.of_int (117)) (Prims.of_int (66)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___5)
@@ -989,7 +989,7 @@ let (acomp_to_string :
(Prims.of_int (117)) (Prims.of_int (72)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___4)
@@ -1006,7 +1006,7 @@ let (acomp_to_string :
(Prims.of_int (117)) (Prims.of_int (72)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___3)
@@ -1022,7 +1022,7 @@ let (acomp_to_string :
(Prims.of_int (117)) (Prims.of_int (72)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___)
(fun uu___1 ->
@@ -1046,7 +1046,7 @@ let (acomp_to_string :
(Prims.of_int (120)) (Prims.of_int (29)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___4)
@@ -1062,7 +1062,7 @@ let (acomp_to_string :
(Prims.of_int (120)) (Prims.of_int (35)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___3)
@@ -1151,7 +1151,7 @@ let (acomp_to_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1175,7 +1175,7 @@ let (acomp_to_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1197,7 +1197,7 @@ let (acomp_to_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1222,7 +1222,7 @@ let (acomp_to_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1374,7 +1374,7 @@ let (filter_ascriptions :
(Prims.of_int (175)) (Prims.of_int (92)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___6)
@@ -1391,7 +1391,7 @@ let (filter_ascriptions :
(Prims.of_int (175)) (Prims.of_int (92)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___5)
@@ -1407,7 +1407,7 @@ let (filter_ascriptions :
(Prims.of_int (175)) (Prims.of_int (92)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___2)
(fun uu___3 ->
@@ -1645,7 +1645,7 @@ let (genv_to_string :
(Prims.of_int (248)) (Prims.of_int (34)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___2)
@@ -1759,7 +1759,7 @@ let (genv_to_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1790,7 +1790,7 @@ let (genv_to_string :
(
Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1818,7 +1818,7 @@ let (genv_to_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1848,7 +1848,7 @@ let (genv_to_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1878,7 +1878,7 @@ let (genv_to_string :
(Obj.magic
(
FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1907,7 +1907,7 @@ let (genv_to_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1979,7 +1979,7 @@ let (genv_to_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2005,7 +2005,7 @@ let (genv_to_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
diff --git a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Effectful.ml b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Effectful.ml
index f72090881fb..1803794ba77 100644
--- a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Effectful.ml
+++ b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Effectful.ml
@@ -90,7 +90,7 @@ let (cast_info_to_string :
(Prims.of_int (50)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -109,7 +109,7 @@ let (cast_info_to_string :
(Prims.of_int (56)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -130,7 +130,7 @@ let (cast_info_to_string :
(Prims.of_int (56)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -149,7 +149,7 @@ let (cast_info_to_string :
(Prims.of_int (35)) (Prims.of_int (56)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___4)
@@ -166,7 +166,7 @@ let (cast_info_to_string :
(Prims.of_int (35)) (Prims.of_int (56)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___3)
@@ -181,7 +181,7 @@ let (cast_info_to_string :
(Prims.of_int (56)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
(fun uu___1 ->
@@ -295,7 +295,7 @@ let (effect_info_to_string :
(Prims.of_int (43)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -316,7 +316,7 @@ let (effect_info_to_string :
(Prims.of_int (49)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -338,7 +338,7 @@ let (effect_info_to_string :
(Prims.of_int (49)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -358,7 +358,7 @@ let (effect_info_to_string :
(Prims.of_int (54)) (Prims.of_int (49)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___6)
@@ -375,7 +375,7 @@ let (effect_info_to_string :
(Prims.of_int (54)) (Prims.of_int (49)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___5)
@@ -392,7 +392,7 @@ let (effect_info_to_string :
(Prims.of_int (49)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___2)
(fun uu___3 ->
@@ -406,7 +406,7 @@ let (effect_info_to_string :
(Prims.of_int (49)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___1)
(fun uu___2 ->
@@ -423,7 +423,7 @@ let (effect_info_to_string :
(Prims.of_int (49)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
(fun uu___1 ->
@@ -462,7 +462,7 @@ let (eterm_info_to_string :
(Prims.of_int (66)) (Prims.of_int (56)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___2)
(fun uu___3 ->
@@ -477,7 +477,7 @@ let (eterm_info_to_string :
(Prims.of_int (66)) (Prims.of_int (67)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___1)
(fun uu___2 ->
@@ -554,7 +554,7 @@ let (eterm_info_to_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -578,7 +578,7 @@ let (eterm_info_to_string :
(Prims.of_int (18)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -600,7 +600,7 @@ let (eterm_info_to_string :
(Prims.of_int (18)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -621,7 +621,7 @@ let (eterm_info_to_string :
(Prims.of_int (71)) (Prims.of_int (18)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___2)
@@ -1414,7 +1414,7 @@ let (typ_or_comp_to_effect_info :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1629,7 +1629,7 @@ let (compute_eterm_info :
(
Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2088,7 +2088,7 @@ let (cast_info_to_propositions :
(Prims.of_int (313)) (Prims.of_int (75)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___2)
(fun uu___3 ->
@@ -2772,7 +2772,7 @@ let (compute_pre_type :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -3412,7 +3412,7 @@ let (compute_post_type :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -3442,7 +3442,7 @@ let (compute_post_type :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -3472,7 +3472,7 @@ let (compute_post_type :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -3598,7 +3598,7 @@ let (compute_post_type :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -3628,7 +3628,7 @@ let (compute_post_type :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -3658,7 +3658,7 @@ let (compute_post_type :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -3825,7 +3825,7 @@ let (compute_post_type :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -4412,7 +4412,7 @@ let rec (_introduce_variables_for_abs :
(Prims.of_int (68)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -4658,7 +4658,7 @@ let (is_st_get :
(Prims.of_int (511)) (Prims.of_int (53)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___2)
(fun uu___3 ->
@@ -4900,7 +4900,7 @@ let (is_let_st_get :
(Prims.of_int (528)) (Prims.of_int (57)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___2)
(fun uu___3 ->
@@ -5307,7 +5307,7 @@ let rec (find_mem_in_related :
(Prims.of_int (66)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -5759,7 +5759,7 @@ let (pre_post_to_propositions :
(Prims.of_int (83)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -5832,7 +5832,7 @@ let (pre_post_to_propositions :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -7702,7 +7702,7 @@ let (eterm_info_to_assertions :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -7796,7 +7796,7 @@ let (eterm_info_to_assertions :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -8013,7 +8013,7 @@ let (eterm_info_to_assertions :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -8107,7 +8107,7 @@ let (eterm_info_to_assertions :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -8201,7 +8201,7 @@ let (eterm_info_to_assertions :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -8329,7 +8329,7 @@ let (eterm_info_to_assertions :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -8477,7 +8477,7 @@ let (eterm_info_to_assertions :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -8506,7 +8506,7 @@ let (eterm_info_to_assertions :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -8536,7 +8536,7 @@ let (eterm_info_to_assertions :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -8760,7 +8760,7 @@ let (eterm_info_to_assertions :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -9460,7 +9460,7 @@ let (eterm_info_to_assertions :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -9553,7 +9553,7 @@ let (eterm_info_to_assertions :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -10073,7 +10073,7 @@ let (eterm_info_to_assertions :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -10167,7 +10167,7 @@ let (eterm_info_to_assertions :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
diff --git a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_ExploreTerm.ml b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_ExploreTerm.ml
index 9b6d8e3697e..249109268e0 100644
--- a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_ExploreTerm.ml
+++ b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_ExploreTerm.ml
@@ -126,7 +126,7 @@ let (type_info_to_string :
(Prims.of_int (85)) (Prims.of_int (44)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___5)
@@ -142,7 +142,7 @@ let (type_info_to_string :
(Prims.of_int (85)) (Prims.of_int (50)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___4)
@@ -159,7 +159,7 @@ let (type_info_to_string :
(Prims.of_int (85)) (Prims.of_int (50)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___3)
@@ -174,7 +174,7 @@ let (type_info_to_string :
(Prims.of_int (50)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
(fun uu___1 ->
@@ -575,7 +575,7 @@ let (typ_or_comp_to_string :
(Prims.of_int (163)) (Prims.of_int (88)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___5)
@@ -594,7 +594,7 @@ let (typ_or_comp_to_string :
(Prims.of_int (164)) (Prims.of_int (37)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___4)
@@ -611,7 +611,7 @@ let (typ_or_comp_to_string :
(Prims.of_int (164)) (Prims.of_int (37)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___3)
@@ -628,7 +628,7 @@ let (typ_or_comp_to_string :
(Prims.of_int (164)) (Prims.of_int (37)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___)
(fun uu___1 ->
@@ -668,7 +668,7 @@ let (typ_or_comp_to_string :
(Prims.of_int (166)) (Prims.of_int (90)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___5)
@@ -687,7 +687,7 @@ let (typ_or_comp_to_string :
(Prims.of_int (167)) (Prims.of_int (37)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___4)
@@ -704,7 +704,7 @@ let (typ_or_comp_to_string :
(Prims.of_int (167)) (Prims.of_int (37)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___3)
@@ -721,7 +721,7 @@ let (typ_or_comp_to_string :
(Prims.of_int (167)) (Prims.of_int (37)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___)
(fun uu___1 ->
@@ -784,7 +784,7 @@ let (safe_typ_or_comp :
(Prims.of_int (49)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -803,7 +803,7 @@ let (safe_typ_or_comp :
(Prims.of_int (187)) (Prims.of_int (34)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___5)
@@ -820,7 +820,7 @@ let (safe_typ_or_comp :
(Prims.of_int (187)) (Prims.of_int (34)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___4)
@@ -908,7 +908,7 @@ let (safe_typ_or_comp :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -932,7 +932,7 @@ let (safe_typ_or_comp :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -952,7 +952,7 @@ let (safe_typ_or_comp :
(Prims.of_int (192)) (Prims.of_int (50)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___5)
@@ -969,7 +969,7 @@ let (safe_typ_or_comp :
(Prims.of_int (192)) (Prims.of_int (50)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___4)
@@ -1281,7 +1281,7 @@ let rec (unfold_until_arrow :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1591,7 +1591,7 @@ let rec (unfold_until_arrow :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1681,7 +1681,7 @@ let rec (unfold_until_arrow :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2004,7 +2004,7 @@ let (_abs_update_typ :
(Prims.of_int (79)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2643,7 +2643,7 @@ let rec (_flush_typ_or_comp_comp :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2673,7 +2673,7 @@ let rec (_flush_typ_or_comp_comp :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2703,7 +2703,7 @@ let rec (_flush_typ_or_comp_comp :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2732,7 +2732,7 @@ let rec (_flush_typ_or_comp_comp :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2948,7 +2948,7 @@ let (flush_typ_or_comp :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -3076,7 +3076,7 @@ let (safe_arg_typ_or_comp :
(Prims.of_int (386)) (Prims.of_int (61)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___2)
(fun uu___3 ->
@@ -3163,7 +3163,7 @@ let (safe_arg_typ_or_comp :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -3377,7 +3377,7 @@ let (safe_arg_typ_or_comp :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -3637,7 +3637,7 @@ let rec (explore_term :
(Prims.of_int (84)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -3660,7 +3660,7 @@ let rec (explore_term :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -3680,7 +3680,7 @@ let rec (explore_term :
(Prims.of_int (470)) (Prims.of_int (84)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___2)
@@ -3887,7 +3887,7 @@ let rec (explore_term :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
diff --git a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Output.ml b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Output.ml
index daa93aca270..d87c6e1ce98 100644
--- a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Output.ml
+++ b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_Output.ml
@@ -41,7 +41,7 @@ let (subst_shadowed_with_abs_in_assertions :
(Prims.of_int (44)) (Prims.of_int (79)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___2)
(fun uu___3 ->
@@ -262,7 +262,7 @@ let (subst_shadowed_with_abs_in_assertions :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -291,7 +291,7 @@ let (subst_shadowed_with_abs_in_assertions :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -321,7 +321,7 @@ let (subst_shadowed_with_abs_in_assertions :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -351,7 +351,7 @@ let (subst_shadowed_with_abs_in_assertions :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -479,7 +479,7 @@ let (subst_shadowed_with_abs_in_assertions :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -567,7 +567,7 @@ let (subst_shadowed_with_abs_in_assertions :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1080,7 +1080,7 @@ let (propositions_to_printout :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1341,7 +1341,7 @@ let (result_to_printout :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1390,7 +1390,7 @@ let (result_to_printout :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1414,7 +1414,7 @@ let (result_to_printout :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1481,7 +1481,7 @@ let (_debug_print_var :
(Prims.of_int (157)) (Prims.of_int (62)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___4)
(fun uu___5 ->
@@ -1496,7 +1496,7 @@ let (_debug_print_var :
(Prims.of_int (157)) (Prims.of_int (62)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___3)
(fun uu___4 ->
@@ -1510,7 +1510,7 @@ let (_debug_print_var :
(Prims.of_int (157)) (Prims.of_int (62)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___2)
(fun uu___3 ->
@@ -1601,7 +1601,7 @@ let (_debug_print_var :
(Prims.of_int (50)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1671,7 +1671,7 @@ let (_debug_print_var :
(Prims.of_int (41)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1797,7 +1797,7 @@ let (_debug_print_var :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1831,7 +1831,7 @@ let (_debug_print_var :
FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1955,7 +1955,7 @@ let (pp_tac : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) =
(Prims.of_int (184)) (Prims.of_int (61)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___3)
(fun uu___4 ->
diff --git a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_PostProcess.ml b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_PostProcess.ml
index ca20c5bbaf1..e65d3c26526 100644
--- a/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_PostProcess.ml
+++ b/ocaml/fstar-lib/generated/FStar_InteractiveHelpers_PostProcess.ml
@@ -100,7 +100,7 @@ let (pp_explore :
(Prims.of_int (54)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -259,7 +259,7 @@ let (pp_explore :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -666,7 +666,7 @@ let find_predicated_term_explorer :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -690,7 +690,7 @@ let find_predicated_term_explorer :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -713,7 +713,7 @@ let find_predicated_term_explorer :
(Prims.of_int (95)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -927,7 +927,7 @@ let (find_focused_term_in_current_goal :
(Prims.of_int (79)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1077,7 +1077,7 @@ let (find_focused_term_in_current_goal :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1206,7 +1206,7 @@ let (find_focused_term_in_current_goal :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1301,7 +1301,7 @@ let (find_focused_term_in_current_goal :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1413,7 +1413,7 @@ let (find_focused_assert_in_current_goal :
(Prims.of_int (68)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1600,7 +1600,7 @@ let (find_focused_assert_in_current_goal :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1764,7 +1764,7 @@ let (analyze_effectful_term :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1997,7 +1997,7 @@ let (analyze_effectful_term :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2331,7 +2331,7 @@ let (analyze_effectful_term :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2405,7 +2405,7 @@ let (analyze_effectful_term :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -3140,7 +3140,7 @@ let (split_conjunctions_under_match :
(Prims.of_int (315)) (Prims.of_int (74)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___3)
@@ -3527,7 +3527,7 @@ let (is_eq :
(Prims.of_int (372)) (Prims.of_int (48)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___3)
@@ -3612,7 +3612,7 @@ let (is_eq :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -3689,7 +3689,7 @@ let (is_eq :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -3953,7 +3953,7 @@ let (is_equality_for_term :
(Prims.of_int (429)) (Prims.of_int (48)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___7)
@@ -3973,7 +3973,7 @@ let (is_equality_for_term :
(Prims.of_int (48)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -3992,7 +3992,7 @@ let (is_equality_for_term :
(Prims.of_int (429)) (Prims.of_int (48)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___3)
(fun uu___4 ->
@@ -4007,7 +4007,7 @@ let (is_equality_for_term :
(Prims.of_int (429)) (Prims.of_int (48)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___2)
(fun uu___3 ->
@@ -4197,7 +4197,7 @@ let (is_equality_for_term :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -4224,7 +4224,7 @@ let (is_equality_for_term :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -4252,7 +4252,7 @@ let (is_equality_for_term :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -4489,7 +4489,7 @@ let (find_subequality :
(Prims.of_int (459)) (Prims.of_int (49)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___7)
@@ -4509,7 +4509,7 @@ let (find_subequality :
(Prims.of_int (49)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -4528,7 +4528,7 @@ let (find_subequality :
(Prims.of_int (459)) (Prims.of_int (49)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___3)
(fun uu___4 ->
@@ -4543,7 +4543,7 @@ let (find_subequality :
(Prims.of_int (459)) (Prims.of_int (49)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___2)
(fun uu___3 ->
@@ -4619,7 +4619,7 @@ let (find_subequality :
(Prims.of_int (73)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -4798,7 +4798,7 @@ let (find_equality_from_post :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -5020,7 +5020,7 @@ let rec (find_context_equality_aux :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -5045,7 +5045,7 @@ let rec (find_context_equality_aux :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -5070,7 +5070,7 @@ let rec (find_context_equality_aux :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -5095,7 +5095,7 @@ let rec (find_context_equality_aux :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -5118,7 +5118,7 @@ let rec (find_context_equality_aux :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -6094,7 +6094,7 @@ let (unfold_in_assert_or_assume :
(Prims.of_int (601)) (Prims.of_int (77)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___2)
(fun uu___3 ->
@@ -6250,7 +6250,7 @@ let (unfold_in_assert_or_assume :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -6482,7 +6482,7 @@ let (unfold_in_assert_or_assume :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -6512,7 +6512,7 @@ let (unfold_in_assert_or_assume :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -6542,7 +6542,7 @@ let (unfold_in_assert_or_assume :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -6572,7 +6572,7 @@ let (unfold_in_assert_or_assume :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -6602,7 +6602,7 @@ let (unfold_in_assert_or_assume :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -6631,7 +6631,7 @@ let (unfold_in_assert_or_assume :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -6845,7 +6845,7 @@ let (unfold_in_assert_or_assume :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -6875,7 +6875,7 @@ let (unfold_in_assert_or_assume :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -6905,7 +6905,7 @@ let (unfold_in_assert_or_assume :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -6935,7 +6935,7 @@ let (unfold_in_assert_or_assume :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -6965,7 +6965,7 @@ let (unfold_in_assert_or_assume :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -6994,7 +6994,7 @@ let (unfold_in_assert_or_assume :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -7233,7 +7233,7 @@ let (unfold_in_assert_or_assume :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -7262,7 +7262,7 @@ let (unfold_in_assert_or_assume :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -7292,7 +7292,7 @@ let (unfold_in_assert_or_assume :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -7322,7 +7322,7 @@ let (unfold_in_assert_or_assume :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -7353,7 +7353,7 @@ let (unfold_in_assert_or_assume :
FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -7584,7 +7584,7 @@ let (unfold_in_assert_or_assume :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -7729,7 +7729,7 @@ let (unfold_in_assert_or_assume :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -7876,7 +7876,7 @@ let (unfold_in_assert_or_assume :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -8435,7 +8435,7 @@ let (unfold_in_assert_or_assume :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -8537,7 +8537,7 @@ let (unfold_in_assert_or_assume :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -8566,7 +8566,7 @@ let (unfold_in_assert_or_assume :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -8727,7 +8727,7 @@ let (unfold_in_assert_or_assume :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
diff --git a/ocaml/fstar-lib/generated/FStar_Options.ml b/ocaml/fstar-lib/generated/FStar_Options.ml
index 86e097be36a..bd4bdc7915a 100644
--- a/ocaml/fstar-lib/generated/FStar_Options.ml
+++ b/ocaml/fstar-lib/generated/FStar_Options.ml
@@ -1990,7 +1990,7 @@ let rec (specs_with_types :
let uu___127
=
text
- "Use a custom prims.fst file. Do not use if you do not know exactly what you're doing." in
+ "Use a custom Prims.fst file. Do not use if you do not know exactly what you're doing." in
(FStar_Getopt.noshort,
"prims",
(PathStr
@@ -3944,7 +3944,7 @@ let (prims : unit -> Prims.string) =
let uu___1 = get_prims () in
match uu___1 with
| FStar_Pervasives_Native.None ->
- let filename = "prims.fst" in
+ let filename = "Prims.fst" in
let uu___2 = find_file filename in
(match uu___2 with
| FStar_Pervasives_Native.Some result -> result
diff --git a/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml b/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml
index 2e7a26b4388..1db21a42d54 100644
--- a/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml
+++ b/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml
@@ -912,16 +912,12 @@ let (check_module_declaration_against_filename :
fun filename ->
let k' = string_of_lid lid true in
let uu___ =
- (let uu___1 =
- let uu___2 =
- let uu___3 = FStar_Compiler_Util.basename filename in
- check_and_strip_suffix uu___3 in
- FStar_Compiler_Util.must uu___2 in
- uu___1 <> k') &&
- (let uu___1 =
- let uu___2 = FStar_Compiler_Util.basename filename in
- uu___2 = "prims.fst" in
- Prims.op_Negation uu___1) in
+ let uu___1 =
+ let uu___2 =
+ let uu___3 = FStar_Compiler_Util.basename filename in
+ check_and_strip_suffix uu___3 in
+ FStar_Compiler_Util.must uu___2 in
+ uu___1 <> k' in
if uu___
then
let uu___1 =
diff --git a/ocaml/fstar-lib/generated/FStar_Reflection_V1_Formula.ml b/ocaml/fstar-lib/generated/FStar_Reflection_V1_Formula.ml
index 536167e27f5..041297ebca6 100644
--- a/ocaml/fstar-lib/generated/FStar_Reflection_V1_Formula.ml
+++ b/ocaml/fstar-lib/generated/FStar_Reflection_V1_Formula.ml
@@ -883,7 +883,7 @@ let (formula_to_string :
(Prims.of_int (60)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -904,7 +904,7 @@ let (formula_to_string :
(Prims.of_int (66)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -970,7 +970,7 @@ let (formula_to_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -992,7 +992,7 @@ let (formula_to_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1015,7 +1015,7 @@ let (formula_to_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1037,7 +1037,7 @@ let (formula_to_string :
(Prims.of_int (80)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1058,7 +1058,7 @@ let (formula_to_string :
(Prims.of_int (80)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1077,7 +1077,7 @@ let (formula_to_string :
(Prims.of_int (215)) (Prims.of_int (80)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -1112,7 +1112,7 @@ let (formula_to_string :
(Prims.of_int (60)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1133,7 +1133,7 @@ let (formula_to_string :
(Prims.of_int (66)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1199,7 +1199,7 @@ let (formula_to_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1221,7 +1221,7 @@ let (formula_to_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1244,7 +1244,7 @@ let (formula_to_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1266,7 +1266,7 @@ let (formula_to_string :
(Prims.of_int (80)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1287,7 +1287,7 @@ let (formula_to_string :
(Prims.of_int (80)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1306,7 +1306,7 @@ let (formula_to_string :
(Prims.of_int (220)) (Prims.of_int (80)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -1349,7 +1349,7 @@ let (formula_to_string :
(Prims.of_int (73)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1369,7 +1369,7 @@ let (formula_to_string :
(Prims.of_int (79)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1390,7 +1390,7 @@ let (formula_to_string :
(Prims.of_int (79)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1409,7 +1409,7 @@ let (formula_to_string :
(Prims.of_int (221)) (Prims.of_int (79)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -1452,7 +1452,7 @@ let (formula_to_string :
(Prims.of_int (73)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1472,7 +1472,7 @@ let (formula_to_string :
(Prims.of_int (79)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1493,7 +1493,7 @@ let (formula_to_string :
(Prims.of_int (79)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1512,7 +1512,7 @@ let (formula_to_string :
(Prims.of_int (222)) (Prims.of_int (79)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -1555,7 +1555,7 @@ let (formula_to_string :
(Prims.of_int (73)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1575,7 +1575,7 @@ let (formula_to_string :
(Prims.of_int (79)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1596,7 +1596,7 @@ let (formula_to_string :
(Prims.of_int (79)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1615,7 +1615,7 @@ let (formula_to_string :
(Prims.of_int (223)) (Prims.of_int (79)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -1658,7 +1658,7 @@ let (formula_to_string :
(Prims.of_int (73)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1678,7 +1678,7 @@ let (formula_to_string :
(Prims.of_int (79)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1699,7 +1699,7 @@ let (formula_to_string :
(Prims.of_int (79)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1718,7 +1718,7 @@ let (formula_to_string :
(Prims.of_int (224)) (Prims.of_int (79)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -1761,7 +1761,7 @@ let (formula_to_string :
(Prims.of_int (70)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1781,7 +1781,7 @@ let (formula_to_string :
(Prims.of_int (76)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1802,7 +1802,7 @@ let (formula_to_string :
(Prims.of_int (76)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1821,7 +1821,7 @@ let (formula_to_string :
(Prims.of_int (225)) (Prims.of_int (76)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -1864,7 +1864,7 @@ let (formula_to_string :
(Prims.of_int (70)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1884,7 +1884,7 @@ let (formula_to_string :
(Prims.of_int (76)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1905,7 +1905,7 @@ let (formula_to_string :
(Prims.of_int (76)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1924,7 +1924,7 @@ let (formula_to_string :
(Prims.of_int (226)) (Prims.of_int (76)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -1967,7 +1967,7 @@ let (formula_to_string :
(Prims.of_int (79)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1987,7 +1987,7 @@ let (formula_to_string :
(Prims.of_int (85)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2008,7 +2008,7 @@ let (formula_to_string :
(Prims.of_int (85)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2027,7 +2027,7 @@ let (formula_to_string :
(Prims.of_int (227)) (Prims.of_int (85)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -2048,7 +2048,7 @@ let (formula_to_string :
(Prims.of_int (228)) (Prims.of_int (42)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___1)
@@ -2064,7 +2064,7 @@ let (formula_to_string :
(Prims.of_int (228)) (Prims.of_int (48)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -2107,7 +2107,7 @@ let (formula_to_string :
(Prims.of_int (71)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2127,7 +2127,7 @@ let (formula_to_string :
(Prims.of_int (77)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2148,7 +2148,7 @@ let (formula_to_string :
(Prims.of_int (77)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2167,7 +2167,7 @@ let (formula_to_string :
(Prims.of_int (229)) (Prims.of_int (77)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -2188,7 +2188,7 @@ let (formula_to_string :
(Prims.of_int (230)) (Prims.of_int (61)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___1)
@@ -2204,7 +2204,7 @@ let (formula_to_string :
(Prims.of_int (230)) (Prims.of_int (67)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -2225,7 +2225,7 @@ let (formula_to_string :
(Prims.of_int (231)) (Prims.of_int (61)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___1)
@@ -2241,7 +2241,7 @@ let (formula_to_string :
(Prims.of_int (231)) (Prims.of_int (67)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -2284,7 +2284,7 @@ let (formula_to_string :
(Prims.of_int (71)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2304,7 +2304,7 @@ let (formula_to_string :
(Prims.of_int (77)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2325,7 +2325,7 @@ let (formula_to_string :
(Prims.of_int (77)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2344,7 +2344,7 @@ let (formula_to_string :
(Prims.of_int (232)) (Prims.of_int (77)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -2365,7 +2365,7 @@ let (formula_to_string :
(Prims.of_int (233)) (Prims.of_int (44)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___1)
@@ -2381,7 +2381,7 @@ let (formula_to_string :
(Prims.of_int (233)) (Prims.of_int (50)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
diff --git a/ocaml/fstar-lib/generated/FStar_Reflection_V2_Formula.ml b/ocaml/fstar-lib/generated/FStar_Reflection_V2_Formula.ml
index 84203835d8b..ec3811e70ff 100644
--- a/ocaml/fstar-lib/generated/FStar_Reflection_V2_Formula.ml
+++ b/ocaml/fstar-lib/generated/FStar_Reflection_V2_Formula.ml
@@ -1190,7 +1190,7 @@ let (formula_to_string :
(Prims.of_int (60)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1211,7 +1211,7 @@ let (formula_to_string :
(Prims.of_int (66)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1277,7 +1277,7 @@ let (formula_to_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1299,7 +1299,7 @@ let (formula_to_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1322,7 +1322,7 @@ let (formula_to_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1344,7 +1344,7 @@ let (formula_to_string :
(Prims.of_int (80)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1365,7 +1365,7 @@ let (formula_to_string :
(Prims.of_int (80)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1384,7 +1384,7 @@ let (formula_to_string :
(Prims.of_int (233)) (Prims.of_int (80)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -1419,7 +1419,7 @@ let (formula_to_string :
(Prims.of_int (60)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1440,7 +1440,7 @@ let (formula_to_string :
(Prims.of_int (66)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1506,7 +1506,7 @@ let (formula_to_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1528,7 +1528,7 @@ let (formula_to_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1551,7 +1551,7 @@ let (formula_to_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1573,7 +1573,7 @@ let (formula_to_string :
(Prims.of_int (80)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1594,7 +1594,7 @@ let (formula_to_string :
(Prims.of_int (80)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1613,7 +1613,7 @@ let (formula_to_string :
(Prims.of_int (238)) (Prims.of_int (80)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -1656,7 +1656,7 @@ let (formula_to_string :
(Prims.of_int (73)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1676,7 +1676,7 @@ let (formula_to_string :
(Prims.of_int (79)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1697,7 +1697,7 @@ let (formula_to_string :
(Prims.of_int (79)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1716,7 +1716,7 @@ let (formula_to_string :
(Prims.of_int (239)) (Prims.of_int (79)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -1759,7 +1759,7 @@ let (formula_to_string :
(Prims.of_int (73)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1779,7 +1779,7 @@ let (formula_to_string :
(Prims.of_int (79)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1800,7 +1800,7 @@ let (formula_to_string :
(Prims.of_int (79)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1819,7 +1819,7 @@ let (formula_to_string :
(Prims.of_int (240)) (Prims.of_int (79)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -1862,7 +1862,7 @@ let (formula_to_string :
(Prims.of_int (73)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1882,7 +1882,7 @@ let (formula_to_string :
(Prims.of_int (79)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1903,7 +1903,7 @@ let (formula_to_string :
(Prims.of_int (79)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1922,7 +1922,7 @@ let (formula_to_string :
(Prims.of_int (241)) (Prims.of_int (79)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -1965,7 +1965,7 @@ let (formula_to_string :
(Prims.of_int (73)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1985,7 +1985,7 @@ let (formula_to_string :
(Prims.of_int (79)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2006,7 +2006,7 @@ let (formula_to_string :
(Prims.of_int (79)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2025,7 +2025,7 @@ let (formula_to_string :
(Prims.of_int (242)) (Prims.of_int (79)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -2068,7 +2068,7 @@ let (formula_to_string :
(Prims.of_int (70)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2088,7 +2088,7 @@ let (formula_to_string :
(Prims.of_int (76)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2109,7 +2109,7 @@ let (formula_to_string :
(Prims.of_int (76)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2128,7 +2128,7 @@ let (formula_to_string :
(Prims.of_int (243)) (Prims.of_int (76)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -2171,7 +2171,7 @@ let (formula_to_string :
(Prims.of_int (70)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2191,7 +2191,7 @@ let (formula_to_string :
(Prims.of_int (76)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2212,7 +2212,7 @@ let (formula_to_string :
(Prims.of_int (76)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2231,7 +2231,7 @@ let (formula_to_string :
(Prims.of_int (244)) (Prims.of_int (76)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -2274,7 +2274,7 @@ let (formula_to_string :
(Prims.of_int (79)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2294,7 +2294,7 @@ let (formula_to_string :
(Prims.of_int (85)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2315,7 +2315,7 @@ let (formula_to_string :
(Prims.of_int (85)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2334,7 +2334,7 @@ let (formula_to_string :
(Prims.of_int (245)) (Prims.of_int (85)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -2355,7 +2355,7 @@ let (formula_to_string :
(Prims.of_int (246)) (Prims.of_int (42)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___1)
@@ -2371,7 +2371,7 @@ let (formula_to_string :
(Prims.of_int (246)) (Prims.of_int (48)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -2414,7 +2414,7 @@ let (formula_to_string :
(Prims.of_int (71)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2434,7 +2434,7 @@ let (formula_to_string :
(Prims.of_int (77)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2455,7 +2455,7 @@ let (formula_to_string :
(Prims.of_int (77)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2474,7 +2474,7 @@ let (formula_to_string :
(Prims.of_int (247)) (Prims.of_int (77)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -2495,7 +2495,7 @@ let (formula_to_string :
(Prims.of_int (248)) (Prims.of_int (61)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___1)
@@ -2511,7 +2511,7 @@ let (formula_to_string :
(Prims.of_int (248)) (Prims.of_int (67)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -2532,7 +2532,7 @@ let (formula_to_string :
(Prims.of_int (249)) (Prims.of_int (61)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___1)
@@ -2548,7 +2548,7 @@ let (formula_to_string :
(Prims.of_int (249)) (Prims.of_int (67)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -2591,7 +2591,7 @@ let (formula_to_string :
(Prims.of_int (71)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2611,7 +2611,7 @@ let (formula_to_string :
(Prims.of_int (77)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2632,7 +2632,7 @@ let (formula_to_string :
(Prims.of_int (77)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2651,7 +2651,7 @@ let (formula_to_string :
(Prims.of_int (250)) (Prims.of_int (77)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -2672,7 +2672,7 @@ let (formula_to_string :
(Prims.of_int (251)) (Prims.of_int (48)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___1)
@@ -2688,7 +2688,7 @@ let (formula_to_string :
(Prims.of_int (251)) (Prims.of_int (54)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_BV.ml b/ocaml/fstar-lib/generated/FStar_Tactics_BV.ml
index c36973c8581..e5580b6d04e 100644
--- a/ocaml/fstar-lib/generated/FStar_Tactics_BV.ml
+++ b/ocaml/fstar-lib/generated/FStar_Tactics_BV.ml
@@ -1317,7 +1317,7 @@ let (arith_to_bv_tac : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) =
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Canon.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Canon.ml
index d1550d40b60..3f0f8af9ef2 100644
--- a/ocaml/fstar-lib/generated/FStar_Tactics_Canon.ml
+++ b/ocaml/fstar-lib/generated/FStar_Tactics_Canon.ml
@@ -1376,7 +1376,7 @@ let (canon_point_entry : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr)
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_CanonCommMonoidSimple.ml b/ocaml/fstar-lib/generated/FStar_Tactics_CanonCommMonoidSimple.ml
index e2041501d63..023a95d3ab0 100644
--- a/ocaml/fstar-lib/generated/FStar_Tactics_CanonCommMonoidSimple.ml
+++ b/ocaml/fstar-lib/generated/FStar_Tactics_CanonCommMonoidSimple.ml
@@ -913,7 +913,7 @@ let canon_monoid :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_MkProjectors.ml b/ocaml/fstar-lib/generated/FStar_Tactics_MkProjectors.ml
index 5420ca747cc..687dda88955 100644
--- a/ocaml/fstar-lib/generated/FStar_Tactics_MkProjectors.ml
+++ b/ocaml/fstar-lib/generated/FStar_Tactics_MkProjectors.ml
@@ -715,7 +715,7 @@ let (mk_proj_decl :
(Prims.of_int (60)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -758,7 +758,7 @@ let (mk_proj_decl :
(Prims.of_int (61)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -926,7 +926,7 @@ let (mk_proj_decl :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -956,7 +956,7 @@ let (mk_proj_decl :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -986,7 +986,7 @@ let (mk_proj_decl :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1280,7 +1280,7 @@ let (mk_proj_decl :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Parametricity.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Parametricity.ml
index 02c2cd3821d..20747ac852a 100644
--- a/ocaml/fstar-lib/generated/FStar_Tactics_Parametricity.ml
+++ b/ocaml/fstar-lib/generated/FStar_Tactics_Parametricity.ml
@@ -1480,7 +1480,7 @@ and (param_fv :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1715,7 +1715,7 @@ and (param_fv :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2986,7 +2986,7 @@ let (param_ctor :
(Prims.of_int (36)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -4405,7 +4405,7 @@ let (paramd :
(Prims.of_int (339)) (Prims.of_int (61)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___6)
diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_PatternMatching.ml b/ocaml/fstar-lib/generated/FStar_Tactics_PatternMatching.ml
index 26c14b969f7..6cff4c935aa 100644
--- a/ocaml/fstar-lib/generated/FStar_Tactics_PatternMatching.ml
+++ b/ocaml/fstar-lib/generated/FStar_Tactics_PatternMatching.ml
@@ -783,7 +783,7 @@ let (string_of_match_exception :
(Prims.of_int (228)) (Prims.of_int (54)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___3)
@@ -799,7 +799,7 @@ let (string_of_match_exception :
(Prims.of_int (228)) (Prims.of_int (54)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___2)
@@ -816,7 +816,7 @@ let (string_of_match_exception :
(Prims.of_int (228)) (Prims.of_int (54)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___1)
@@ -865,7 +865,7 @@ let (string_of_match_exception :
(Prims.of_int (33)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -887,7 +887,7 @@ let (string_of_match_exception :
(Prims.of_int (33)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -907,7 +907,7 @@ let (string_of_match_exception :
(Prims.of_int (232)) (Prims.of_int (33)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___3)
@@ -924,7 +924,7 @@ let (string_of_match_exception :
(Prims.of_int (232)) (Prims.of_int (33)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___2)
@@ -940,7 +940,7 @@ let (string_of_match_exception :
(Prims.of_int (232)) (Prims.of_int (33)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___1)
@@ -985,7 +985,7 @@ let (string_of_match_exception :
(Prims.of_int (43)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1005,7 +1005,7 @@ let (string_of_match_exception :
(Prims.of_int (49)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1026,7 +1026,7 @@ let (string_of_match_exception :
(Prims.of_int (49)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1045,7 +1045,7 @@ let (string_of_match_exception :
(Prims.of_int (235)) (Prims.of_int (49)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___1)
@@ -1069,7 +1069,7 @@ let (string_of_match_exception :
(Prims.of_int (238)) (Prims.of_int (22)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___2)
@@ -1087,7 +1087,7 @@ let (string_of_match_exception :
(Prims.of_int (238)) (Prims.of_int (74)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___1)
@@ -1214,7 +1214,7 @@ let (string_of_bindings :
(Prims.of_int (286)) (Prims.of_int (64)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___4)
@@ -1230,7 +1230,7 @@ let (string_of_bindings :
(Prims.of_int (286)) (Prims.of_int (64)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___3)
@@ -1246,7 +1246,7 @@ let (string_of_bindings :
(Prims.of_int (286)) (Prims.of_int (64)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___2)
(fun uu___3 ->
@@ -1791,7 +1791,7 @@ let (string_of_matching_solution :
(Prims.of_int (385)) (Prims.of_int (44)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___4)
@@ -1807,7 +1807,7 @@ let (string_of_matching_solution :
(Prims.of_int (385)) (Prims.of_int (44)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___3)
@@ -1863,7 +1863,7 @@ let (string_of_matching_solution :
(Prims.of_int (47)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1881,7 +1881,7 @@ let (string_of_matching_solution :
(Prims.of_int (389)) (Prims.of_int (47)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___4)
@@ -1916,7 +1916,7 @@ let (string_of_matching_solution :
(Prims.of_int (389)) (Prims.of_int (60)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___1)
(fun hyps ->
@@ -2052,7 +2052,7 @@ let rec solve_mp_for_single_hyp :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2200,7 +2200,7 @@ let solve_mp :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2815,7 +2815,7 @@ let (matching_problem_of_abs :
(Prims.of_int (636)) (Prims.of_int (71)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___4)
@@ -2899,7 +2899,7 @@ let (matching_problem_of_abs :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2923,7 +2923,7 @@ let (matching_problem_of_abs :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2946,7 +2946,7 @@ let (matching_problem_of_abs :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -3113,7 +3113,7 @@ let (matching_problem_of_abs :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -3142,7 +3142,7 @@ let (matching_problem_of_abs :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -3172,7 +3172,7 @@ let (matching_problem_of_abs :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -3202,7 +3202,7 @@ let (matching_problem_of_abs :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -3232,7 +3232,7 @@ let (matching_problem_of_abs :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -4265,7 +4265,7 @@ let (specialize_abspat_continuation :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -4367,7 +4367,7 @@ let (specialize_abspat_continuation :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Print.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Print.ml
index db0ebf63e0e..1da0e955926 100644
--- a/ocaml/fstar-lib/generated/FStar_Tactics_Print.ml
+++ b/ocaml/fstar-lib/generated/FStar_Tactics_Print.ml
@@ -13,7 +13,7 @@ let (namedv_to_string :
(Prims.of_int (17)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
(fun uu___1 ->
@@ -82,7 +82,7 @@ let rec print_list_aux :
(Prims.of_int (45)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -103,7 +103,7 @@ let rec print_list_aux :
(Prims.of_int (45)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -131,7 +131,7 @@ let print_list :
(Prims.of_int (27)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___1)
(fun uu___2 ->
@@ -145,7 +145,7 @@ let print_list :
(Prims.of_int (33)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
(fun uu___1 ->
@@ -190,7 +190,7 @@ let rec (universe_to_ast_string :
(Prims.of_int (30)) (Prims.of_int (61)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -209,7 +209,7 @@ let rec (universe_to_ast_string :
(Prims.of_int (31)) (Prims.of_int (64)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
@@ -299,7 +299,7 @@ let rec (term_to_ast_string :
(Prims.of_int (42)) (Prims.of_int (48)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___2)
@@ -318,7 +318,7 @@ let rec (term_to_ast_string :
(Prims.of_int (43)) (Prims.of_int (46)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___2)
@@ -350,7 +350,7 @@ let rec (term_to_ast_string :
(Prims.of_int (75)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -368,7 +368,7 @@ let rec (term_to_ast_string :
(Prims.of_int (46)) (Prims.of_int (75)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___4)
@@ -403,7 +403,7 @@ let rec (term_to_ast_string :
(Prims.of_int (46)) (Prims.of_int (76)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___2)
@@ -445,7 +445,7 @@ let rec (term_to_ast_string :
(Prims.of_int (94)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -468,7 +468,7 @@ let rec (term_to_ast_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -504,7 +504,7 @@ let rec (term_to_ast_string :
(Prims.of_int (47)) (Prims.of_int (95)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___3)
@@ -547,7 +547,7 @@ let rec (term_to_ast_string :
(Prims.of_int (85)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -570,7 +570,7 @@ let rec (term_to_ast_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -606,7 +606,7 @@ let rec (term_to_ast_string :
(Prims.of_int (48)) (Prims.of_int (86)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___2)
@@ -649,7 +649,7 @@ let rec (term_to_ast_string :
(Prims.of_int (89)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -672,7 +672,7 @@ let rec (term_to_ast_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -708,7 +708,7 @@ let rec (term_to_ast_string :
(Prims.of_int (49)) (Prims.of_int (90)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___2)
@@ -745,7 +745,7 @@ let rec (term_to_ast_string :
(Prims.of_int (50)) (Prims.of_int (58)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___2)
@@ -788,7 +788,7 @@ let rec (term_to_ast_string :
(Prims.of_int (91)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -811,7 +811,7 @@ let rec (term_to_ast_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -847,7 +847,7 @@ let rec (term_to_ast_string :
(Prims.of_int (51)) (Prims.of_int (92)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___2)
@@ -929,7 +929,7 @@ let rec (term_to_ast_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -953,7 +953,7 @@ let rec (term_to_ast_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -978,7 +978,7 @@ let rec (term_to_ast_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1001,7 +1001,7 @@ let rec (term_to_ast_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1023,7 +1023,7 @@ let rec (term_to_ast_string :
(Prims.of_int (51)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1041,7 +1041,7 @@ let rec (term_to_ast_string :
(Prims.of_int (58)) (Prims.of_int (51)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___5)
@@ -1075,7 +1075,7 @@ let rec (term_to_ast_string :
(Prims.of_int (58)) (Prims.of_int (52)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___3)
@@ -1143,7 +1143,7 @@ let rec (term_to_ast_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1167,7 +1167,7 @@ let rec (term_to_ast_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1190,7 +1190,7 @@ let rec (term_to_ast_string :
(Prims.of_int (34)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1213,7 +1213,7 @@ let rec (term_to_ast_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1249,7 +1249,7 @@ let rec (term_to_ast_string :
(Prims.of_int (66)) (Prims.of_int (35)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___2)
@@ -1293,7 +1293,7 @@ let rec (term_to_ast_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1317,7 +1317,7 @@ let rec (term_to_ast_string :
(Prims.of_int (139)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1340,7 +1340,7 @@ let rec (term_to_ast_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1376,7 +1376,7 @@ let rec (term_to_ast_string :
(Prims.of_int (67)) (Prims.of_int (140)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___3)
@@ -1421,7 +1421,7 @@ let rec (term_to_ast_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1445,7 +1445,7 @@ let rec (term_to_ast_string :
(Prims.of_int (139)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1468,7 +1468,7 @@ let rec (term_to_ast_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1504,7 +1504,7 @@ let rec (term_to_ast_string :
(Prims.of_int (68)) (Prims.of_int (140)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___3)
@@ -1555,7 +1555,7 @@ and (match_returns_to_string :
(Prims.of_int (51)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1599,7 +1599,7 @@ and (match_returns_to_string :
(Prims.of_int (80)) (Prims.of_int (23)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___2)
@@ -1659,7 +1659,7 @@ and (match_returns_to_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1707,7 +1707,7 @@ and (match_returns_to_string :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1730,7 +1730,7 @@ and (match_returns_to_string :
(Prims.of_int (78)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1777,7 +1777,7 @@ and (branch_to_ast_string :
(Prims.of_int (91)) (Prims.of_int (40)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___3)
@@ -1816,7 +1816,7 @@ and (comp_to_ast_string :
(Prims.of_int (95)) (Prims.of_int (46)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___)
(fun uu___1 ->
@@ -1832,7 +1832,7 @@ and (comp_to_ast_string :
(Prims.of_int (96)) (Prims.of_int (48)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___)
(fun uu___1 ->
@@ -1865,7 +1865,7 @@ and (comp_to_ast_string :
(Prims.of_int (97)) (Prims.of_int (91)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___5)
@@ -1881,7 +1881,7 @@ and (comp_to_ast_string :
(Prims.of_int (97)) (Prims.of_int (91)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___4)
@@ -1897,7 +1897,7 @@ and (comp_to_ast_string :
(Prims.of_int (97)) (Prims.of_int (91)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___1)
(fun uu___2 ->
@@ -1937,7 +1937,7 @@ and (comp_to_ast_string :
(Prims.of_int (110)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1955,7 +1955,7 @@ and (comp_to_ast_string :
(Prims.of_int (99)) (Prims.of_int (110)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___9)
@@ -1990,7 +1990,7 @@ and (comp_to_ast_string :
(Prims.of_int (99)) (Prims.of_int (111)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___7)
@@ -2007,7 +2007,7 @@ and (comp_to_ast_string :
(Prims.of_int (99)) (Prims.of_int (111)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___6)
@@ -2023,7 +2023,7 @@ and (comp_to_ast_string :
(Prims.of_int (99)) (Prims.of_int (111)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___3)
(fun uu___4 ->
@@ -2037,7 +2037,7 @@ and (comp_to_ast_string :
(Prims.of_int (99)) (Prims.of_int (111)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___2)
(fun uu___3 ->
diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_TypeRepr.ml b/ocaml/fstar-lib/generated/FStar_Tactics_TypeRepr.ml
index a27ff661121..5d85f7385bb 100644
--- a/ocaml/fstar-lib/generated/FStar_Tactics_TypeRepr.ml
+++ b/ocaml/fstar-lib/generated/FStar_Tactics_TypeRepr.ml
@@ -739,7 +739,7 @@ let rec (get_apply_tuple :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -985,7 +985,7 @@ let rec (get_apply_tuple :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1047,7 +1047,7 @@ let rec (get_apply_tuple :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1099,7 +1099,7 @@ let rec (get_apply_tuple :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Typeclasses.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Typeclasses.ml
index dfb9494498a..07af097c260 100644
--- a/ocaml/fstar-lib/generated/FStar_Tactics_Typeclasses.ml
+++ b/ocaml/fstar-lib/generated/FStar_Tactics_Typeclasses.ml
@@ -660,7 +660,7 @@ let (trywith :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -685,7 +685,7 @@ let (trywith :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -710,7 +710,7 @@ let (trywith :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -794,7 +794,7 @@ let (trywith :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -1121,7 +1121,7 @@ let (local :
(Prims.of_int (202)) (Prims.of_int (58)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___3)
@@ -1212,7 +1212,7 @@ let (global :
(Prims.of_int (209)) (Prims.of_int (59)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___3)
@@ -2259,7 +2259,7 @@ let (tcresolve : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) =
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2840,7 +2840,7 @@ let (mk_class :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -2950,7 +2950,7 @@ let (mk_class :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -3119,7 +3119,7 @@ let (mk_class :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -3148,7 +3148,7 @@ let (mk_class :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -3178,7 +3178,7 @@ let (mk_class :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -3382,7 +3382,7 @@ let (mk_class :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -3539,7 +3539,7 @@ let (mk_class :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -4493,7 +4493,7 @@ let (mk_class :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -4558,7 +4558,7 @@ let (mk_class :
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
- "prims.fst"
+ "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Util.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Util.ml
index f5431e303b7..ba9107762ff 100644
--- a/ocaml/fstar-lib/generated/FStar_Tactics_Util.ml
+++ b/ocaml/fstar-lib/generated/FStar_Tactics_Util.ml
@@ -698,7 +698,7 @@ let rec string_of_list :
(Prims.of_int (44)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -719,7 +719,7 @@ let rec string_of_list :
(Prims.of_int (44)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611))
(Prims.of_int (19))
(Prims.of_int (611))
@@ -753,7 +753,7 @@ let string_of_option :
(Prims.of_int (126)) (Prims.of_int (27)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___)
diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Derived.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Derived.ml
index d34366502d8..b832803338e 100644
--- a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Derived.ml
+++ b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Derived.ml
@@ -56,7 +56,7 @@ let (binder_to_string :
(Prims.of_int (50)) (Prims.of_int (80)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___6)
@@ -72,7 +72,7 @@ let (binder_to_string :
(Prims.of_int (50)) (Prims.of_int (86)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___5)
@@ -87,7 +87,7 @@ let (binder_to_string :
(Prims.of_int (50)) (Prims.of_int (86)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst"
+ (FStar_Range.mk_range "Prims.fst"
(Prims.of_int (611)) (Prims.of_int (19))
(Prims.of_int (611)) (Prims.of_int (31)))))
(Obj.magic uu___4)
@@ -105,7 +105,7 @@ let (binder_to_string :
(Prims.of_int (50)) (Prims.of_int (86)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___3)
(fun uu___4 ->
@@ -120,7 +120,7 @@ let (binder_to_string :
(Prims.of_int (50)) (Prims.of_int (86)))))
(FStar_Sealed.seal
(Obj.magic
- (FStar_Range.mk_range "prims.fst" (Prims.of_int (611))
+ (FStar_Range.mk_range "Prims.fst" (Prims.of_int (611))
(Prims.of_int (19)) (Prims.of_int (611))
(Prims.of_int (31))))) (Obj.magic uu___2)
(fun uu___3 ->
diff --git a/src/basic/FStar.Errors.Msg.fsti b/src/basic/FStar.Errors.Msg.fsti
index 0b194b46c42..e30f81a38a3 100644
--- a/src/basic/FStar.Errors.Msg.fsti
+++ b/src/basic/FStar.Errors.Msg.fsti
@@ -10,7 +10,7 @@ these:
* Error 19 at tests/error-messages/Bug1997.fst(92,19-92,49):
- Assertion failed
- The SMT solver could not prove the query. Use --query_stats for more details.
- - Also see: prims.fst(96,32-96,42)
+ - Also see: Prims.fst(96,32-96,42)
The header is taken from the code and range, and then the documents are rendered
in order.
diff --git a/src/basic/FStar.Options.fst b/src/basic/FStar.Options.fst
index 60f53a69cbc..e932d750e16 100644
--- a/src/basic/FStar.Options.fst
+++ b/src/basic/FStar.Options.fst
@@ -1091,7 +1091,7 @@ let rec specs_with_types warn_unsafe : list (char & string & opt_type & Pprint.d
( noshort,
"prims",
PathStr "file",
- text "Use a custom prims.fst file. Do not use if you do not know exactly what you're doing.");
+ text "Use a custom Prims.fst file. Do not use if you do not know exactly what you're doing.");
( noshort,
"print_bound_var_types",
@@ -1791,7 +1791,7 @@ let find_file =
let prims () =
match get_prims() with
| None ->
- let filename = "prims.fst" in
+ let filename = "Prims.fst" in
begin match find_file filename with
| Some result ->
result
diff --git a/src/fstar/FStar.CheckedFiles.fst b/src/fstar/FStar.CheckedFiles.fst
index f728e238a1f..c1bf91deea2 100644
--- a/src/fstar/FStar.CheckedFiles.fst
+++ b/src/fstar/FStar.CheckedFiles.fst
@@ -34,7 +34,7 @@ let dbg = Debug.get_toggle "CheckedFiles"
(*
* We write this version number to the cache files, and
* detect when loading the cache that the version number is same
- * It needs to be kept in sync with prims.fst
+ * It needs to be kept in sync with Prims.fst
*)
let cache_version_number = 70
@@ -282,7 +282,7 @@ let load_checked_file_with_tc_result
* if there exists an interface for it, mark that too as valid
* this is specially needed for extraction invocations of F* with --cmi flag
* for example, consider a scenario:
- * A.fst -> B.fsti -> prims.fst
+ * A.fst -> B.fsti -> Prims.fst
* ^ ^
* | /
* B.fst
@@ -350,7 +350,7 @@ let load_parsing_data_from_cache file_name =
* following is the reason for it:
*
* consider a scenario:
- * A.fst -> B.fsti -> prims.fst
+ * A.fst -> B.fsti -> Prims.fst
* ^ ^
* | /
* B.fst
diff --git a/src/parser/FStar.Parser.Dep.fst b/src/parser/FStar.Parser.Dep.fst
index d3afd007f91..b3b14ac08c4 100644
--- a/src/parser/FStar.Parser.Dep.fst
+++ b/src/parser/FStar.Parser.Dep.fst
@@ -515,9 +515,7 @@ let namespace_of_lid l =
let check_module_declaration_against_filename (lid: lident) (filename: string): unit =
let k' = string_of_lid lid true in
- if must (check_and_strip_suffix (basename filename)) <> k'
- && (not (basename filename = "prims.fst")) (* Exception for module Prims = prims.fst until we switch *)
- then
+ if must (check_and_strip_suffix (basename filename)) <> k' then
log_issue lid Errors.Error_ModuleFileNameMismatch [
Errors.Msg.text (Util.format2 "The module declaration \"module %s\" \
found in file %s does not match its filename." (string_of_lid lid true) filename);
diff --git a/tests/error-messages/ArrowRanges.fst.expected b/tests/error-messages/ArrowRanges.fst.expected
index d1f1d7c4915..f491722fd16 100644
--- a/tests/error-messages/ArrowRanges.fst.expected
+++ b/tests/error-messages/ArrowRanges.fst.expected
@@ -4,7 +4,7 @@
- Expected type Prims.eqtype got type Type0
- The SMT solver could not prove the query. Use --query_stats for more
details.
- - See also prims.fst(73,23-73,30)
+ - See also Prims.fst(73,23-73,30)
>>]
>> Got issues: [
diff --git a/tests/error-messages/Basic.fst.expected b/tests/error-messages/Basic.fst.expected
index 79e943e5a22..4346e634909 100644
--- a/tests/error-messages/Basic.fst.expected
+++ b/tests/error-messages/Basic.fst.expected
@@ -72,7 +72,7 @@
- Assertion failed
- The SMT solver could not prove the query. Use --query_stats for more
details.
- - See also prims.fst(451,90-451,102)
+ - See also Prims.fst(451,90-451,102)
>>]
>> Got issues: [
@@ -80,7 +80,7 @@
- Assertion failed
- The SMT solver could not prove the query. Use --query_stats for more
details.
- - See also prims.fst(451,90-451,102)
+ - See also Prims.fst(451,90-451,102)
>>]
>> Got issues: [
@@ -88,7 +88,7 @@
- Assertion failed
- The SMT solver could not prove the query. Use --query_stats for more
details.
- - See also prims.fst(451,90-451,102)
+ - See also Prims.fst(451,90-451,102)
>>]
Verified module: Basic
diff --git a/tests/error-messages/Coercions.fst.expected b/tests/error-messages/Coercions.fst.expected
index d8ef22a12b9..2d664d34201 100644
--- a/tests/error-messages/Coercions.fst.expected
+++ b/tests/error-messages/Coercions.fst.expected
@@ -20,7 +20,7 @@
- Expected type Prims.nat got type Prims.int
- The SMT solver could not prove the query. Use --query_stats for more
details.
- - See also prims.fst(680,18-680,24)
+ - See also Prims.fst(680,18-680,24)
>>]
>> Got issues: [
@@ -29,7 +29,7 @@
- Expected type Prims.nat got type Prims.int
- The SMT solver could not prove the query. Use --query_stats for more
details.
- - See also prims.fst(680,18-680,24)
+ - See also Prims.fst(680,18-680,24)
>>]
>> Got issues: [
@@ -38,7 +38,7 @@
- Expected type Prims.nat got type Prims.int
- The SMT solver could not prove the query. Use --query_stats for more
details.
- - See also prims.fst(680,18-680,24)
+ - See also Prims.fst(680,18-680,24)
>>]
>> Got issues: [
@@ -47,7 +47,7 @@
- Expected type Prims.nat got type Prims.int
- The SMT solver could not prove the query. Use --query_stats for more
details.
- - See also prims.fst(680,18-680,24)
+ - See also Prims.fst(680,18-680,24)
>>]
>> Got issues: [
@@ -56,7 +56,7 @@
- Expected type Prims.nat got type Prims.int
- The SMT solver could not prove the query. Use --query_stats for more
details.
- - See also prims.fst(680,18-680,24)
+ - See also Prims.fst(680,18-680,24)
>>]
Verified module: Coercions
diff --git a/tests/error-messages/Inference.fst.expected b/tests/error-messages/Inference.fst.expected
index add1ff70a6d..ec67aa3ecd2 100644
--- a/tests/error-messages/Inference.fst.expected
+++ b/tests/error-messages/Inference.fst.expected
@@ -4,14 +4,14 @@
- Expected type Prims.eqtype got type Type0
- The SMT solver could not prove the query. Use --query_stats for more
details.
- - See also prims.fst(73,23-73,30)
+ - See also Prims.fst(73,23-73,30)
* Error 19 at Inference.fst(20,14-20,15):
- Subtyping check failed
- Expected type Prims.eqtype got type Type0
- The SMT solver could not prove the query. Use --query_stats for more
details.
- - See also prims.fst(73,23-73,30)
+ - See also Prims.fst(73,23-73,30)
>>]
Verified module: Inference
diff --git a/tests/error-messages/NegativeTests.False.fst.expected b/tests/error-messages/NegativeTests.False.fst.expected
index e1e41901bc0..4f9ffd74275 100644
--- a/tests/error-messages/NegativeTests.False.fst.expected
+++ b/tests/error-messages/NegativeTests.False.fst.expected
@@ -3,7 +3,7 @@
- Assertion failed
- The SMT solver could not prove the query. Use --query_stats for more
details.
- - See also prims.fst(459,77-459,89)
+ - See also Prims.fst(459,77-459,89)
>>]
>> Got issues: [
diff --git a/tests/error-messages/NegativeTests.Neg.fst.expected b/tests/error-messages/NegativeTests.Neg.fst.expected
index 53a659300aa..eab855117bc 100644
--- a/tests/error-messages/NegativeTests.Neg.fst.expected
+++ b/tests/error-messages/NegativeTests.Neg.fst.expected
@@ -4,7 +4,7 @@
- Expected type Prims.nat got type Prims.int
- The SMT solver could not prove the query. Use --query_stats for more
details.
- - See also prims.fst(680,18-680,24)
+ - See also Prims.fst(680,18-680,24)
>>]
>> Got issues: [
@@ -13,7 +13,7 @@
- Expected type Prims.nat got type Prims.int
- The SMT solver could not prove the query. Use --query_stats for more
details.
- - See also prims.fst(680,18-680,24)
+ - See also Prims.fst(680,18-680,24)
>>]
>> Got issues: [
@@ -72,7 +72,7 @@
- Expected type Prims.nat got type Prims.int
- The SMT solver could not prove the query. Use --query_stats for more
details.
- - See also prims.fst(680,18-680,24)
+ - See also Prims.fst(680,18-680,24)
>>]
>> Got issues: [
diff --git a/tests/error-messages/NegativeTests.ShortCircuiting.fst.expected b/tests/error-messages/NegativeTests.ShortCircuiting.fst.expected
index be8e0c2ee80..c8bcfaf96e7 100644
--- a/tests/error-messages/NegativeTests.ShortCircuiting.fst.expected
+++ b/tests/error-messages/NegativeTests.ShortCircuiting.fst.expected
@@ -12,7 +12,7 @@
- Assertion failed
- The SMT solver could not prove the query. Use --query_stats for more
details.
- - See also prims.fst(451,90-451,102)
+ - See also Prims.fst(451,90-451,102)
>>]
* Warning 240 at NegativeTests.ShortCircuiting.fst(19,4-19,7):
diff --git a/tests/error-messages/NegativeTests.ZZImplicitFalse.fst.expected b/tests/error-messages/NegativeTests.ZZImplicitFalse.fst.expected
index 3b1279b8310..055a8eba343 100644
--- a/tests/error-messages/NegativeTests.ZZImplicitFalse.fst.expected
+++ b/tests/error-messages/NegativeTests.ZZImplicitFalse.fst.expected
@@ -4,7 +4,7 @@
- Expected type Prims.l_False got type Prims.unit
- The SMT solver could not prove the query. Use --query_stats for more
details.
- - See also prims.fst(159,29-159,34)
+ - See also Prims.fst(159,29-159,34)
>>]
* Warning 240 at NegativeTests.ZZImplicitFalse.fst(18,4-18,8):
diff --git a/tests/error-messages/PatAnnot.fst.expected b/tests/error-messages/PatAnnot.fst.expected
index e6dd0e5e571..11959289a15 100644
--- a/tests/error-messages/PatAnnot.fst.expected
+++ b/tests/error-messages/PatAnnot.fst.expected
@@ -12,7 +12,7 @@
- Assertion failed
- The SMT solver could not prove the query. Use --query_stats for more
details.
- - Also see: prims.fst(459,77-459,89)
+ - Also see: Prims.fst(459,77-459,89)
>>]
>> Got issues: [
@@ -20,7 +20,7 @@
- Assertion failed
- The SMT solver could not prove the query. Use --query_stats for more
details.
- - Also see: prims.fst(459,77-459,89)
+ - Also see: Prims.fst(459,77-459,89)
>>]
>> Got issues: [
@@ -38,7 +38,7 @@
- Expected type Prims.nat got type Prims.int
- The SMT solver could not prove the query. Use --query_stats for more
details.
- - See also prims.fst(680,18-680,24)
+ - See also Prims.fst(680,18-680,24)
>>]
>> Got issues: [
@@ -46,7 +46,7 @@
- Type annotation on parameter incompatible with the expected type
- The SMT solver could not prove the query. Use --query_stats for more
details.
- - See also prims.fst(680,18-680,24)
+ - See also Prims.fst(680,18-680,24)
>>]
Verified module: PatAnnot
diff --git a/tests/error-messages/Test.FunctionalExtensionality.fst.expected b/tests/error-messages/Test.FunctionalExtensionality.fst.expected
index c022ebdb02b..f8b5d4d9254 100644
--- a/tests/error-messages/Test.FunctionalExtensionality.fst.expected
+++ b/tests/error-messages/Test.FunctionalExtensionality.fst.expected
@@ -21,7 +21,7 @@
- Expected type _: Prims.int -> Prims.int got type Prims.nat ^-> Prims.int
- The SMT solver could not prove the query. Use --query_stats for more
details.
- - See also prims.fst(680,18-680,24)
+ - See also Prims.fst(680,18-680,24)
>>]
>> Got issues: [
diff --git a/tests/error-messages/TestErrorLocations.fst.expected b/tests/error-messages/TestErrorLocations.fst.expected
index 2c65ad31688..b8a849810a3 100644
--- a/tests/error-messages/TestErrorLocations.fst.expected
+++ b/tests/error-messages/TestErrorLocations.fst.expected
@@ -34,7 +34,7 @@
- Expected type Prims.nat got type Prims.int
- The SMT solver could not prove the query. Use --query_stats for more
details.
- - See also prims.fst(680,18-680,24)
+ - See also Prims.fst(680,18-680,24)
>>]
>> Got issues: [
@@ -50,7 +50,7 @@
- Assertion failed
- The SMT solver could not prove the query. Use --query_stats for more
details.
- - See also prims.fst(451,90-451,102)
+ - See also Prims.fst(451,90-451,102)
>>]
>> Got issues: [
@@ -58,7 +58,7 @@
- Assertion failed
- The SMT solver could not prove the query. Use --query_stats for more
details.
- - See also prims.fst(451,90-451,102)
+ - See also Prims.fst(451,90-451,102)
>>]
>> Got issues: [
@@ -67,7 +67,7 @@
- Expected type Prims.nat got type Prims.int
- The SMT solver could not prove the query. Use --query_stats for more
details.
- - See also prims.fst(680,18-680,24)
+ - See also Prims.fst(680,18-680,24)
>>]
>> Got issues: [
diff --git a/tests/error-messages/WPExtensionality.fst.expected b/tests/error-messages/WPExtensionality.fst.expected
index 06f5a9cefd4..935554ae5e9 100644
--- a/tests/error-messages/WPExtensionality.fst.expected
+++ b/tests/error-messages/WPExtensionality.fst.expected
@@ -3,7 +3,7 @@
- Assertion failed
- The SMT solver could not prove the query. Use --query_stats for more
details.
- - See also prims.fst(451,90-451,102)
+ - See also Prims.fst(451,90-451,102)
>>]
Verified module: WPExtensionality
diff --git a/tests/ide/emacs/Integration.push-pop.out.expected b/tests/ide/emacs/Integration.push-pop.out.expected
index d12bcab93d5..a537345f0a0 100644
--- a/tests/ide/emacs/Integration.push-pop.out.expected
+++ b/tests/ide/emacs/Integration.push-pop.out.expected
@@ -78,17 +78,17 @@
{"kind": "response", "query-id": "80", "response": [], "status": "success"}
{"kind": "response", "query-id": "91", "response": [{"level": "error", "message": "- Syntax error\n", "number": 168, "ranges": [{"beg": [12, 0], "end": [12, 0], "fname": ""}]}], "status": "success"}
{"kind": "response", "query-id": "98", "response": [], "status": "success"}
-{"kind": "response", "query-id": "101", "response": [{"level": "error", "message": "- Subtyping check failed\n- Expected type nat got type int\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also prims.fst(680,18-680,24)\n", "number": 19, "ranges": [{"beg": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [680, 18], "end": [680, 24], "fname": "prims.fst"}]}], "status": "failure"}
+{"kind": "response", "query-id": "101", "response": [{"level": "error", "message": "- Subtyping check failed\n- Expected type nat got type int\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also Prims.fst(680,18-680,24)\n", "number": 19, "ranges": [{"beg": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [680, 18], "end": [680, 24], "fname": "Prims.fst"}]}], "status": "failure"}
{"kind": "response", "query-id": "107", "response": [], "status": "success"}
{"kind": "response", "query-id": "108", "response": [], "status": "success"}
{"kind": "response", "query-id": "112", "response": null, "status": "success"}
{"kind": "response", "query-id": "114", "response": [], "status": "success"}
-{"kind": "response", "query-id": "116", "response": [{"level": "error", "message": "- Subtyping check failed\n- Expected type nat got type int\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also prims.fst(680,18-680,24)\n", "number": 19, "ranges": [{"beg": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [680, 18], "end": [680, 24], "fname": "prims.fst"}]}], "status": "failure"}
+{"kind": "response", "query-id": "116", "response": [{"level": "error", "message": "- Subtyping check failed\n- Expected type nat got type int\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also Prims.fst(680,18-680,24)\n", "number": 19, "ranges": [{"beg": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [680, 18], "end": [680, 24], "fname": "Prims.fst"}]}], "status": "failure"}
{"kind": "response", "query-id": "118", "response": [], "status": "success"}
{"kind": "response", "query-id": "119", "response": [], "status": "success"}
{"kind": "response", "query-id": "122", "response": null, "status": "success"}
{"kind": "response", "query-id": "124", "response": [], "status": "success"}
-{"kind": "response", "query-id": "126", "response": [{"level": "error", "message": "- Subtyping check failed\n- Expected type nat got type int\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also prims.fst(680,18-680,24)\n", "number": 19, "ranges": [{"beg": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [680, 18], "end": [680, 24], "fname": "prims.fst"}]}], "status": "failure"}
+{"kind": "response", "query-id": "126", "response": [{"level": "error", "message": "- Subtyping check failed\n- Expected type nat got type int\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also Prims.fst(680,18-680,24)\n", "number": 19, "ranges": [{"beg": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [680, 18], "end": [680, 24], "fname": "Prims.fst"}]}], "status": "failure"}
{"kind": "response", "query-id": "128", "response": [], "status": "success"}
{"kind": "response", "query-id": "130", "response": [], "status": "success"}
{"kind": "response", "query-id": "133", "response": [], "status": "success"}
@@ -106,7 +106,7 @@
{"kind": "response", "query-id": "191", "response": null, "status": "success"}
{"kind": "response", "query-id": "192", "response": null, "status": "success"}
{"kind": "response", "query-id": "194", "response": [], "status": "success"}
-{"kind": "response", "query-id": "198", "response": [{"level": "error", "message": "- Subtyping check failed\n- Expected type nat got type int\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also prims.fst(680,18-680,24)\n", "number": 19, "ranges": [{"beg": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [680, 18], "end": [680, 24], "fname": "prims.fst"}]}], "status": "failure"}
+{"kind": "response", "query-id": "198", "response": [{"level": "error", "message": "- Subtyping check failed\n- Expected type nat got type int\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also Prims.fst(680,18-680,24)\n", "number": 19, "ranges": [{"beg": [11, 15], "end": [11, 17], "fname": ""}, {"beg": [680, 18], "end": [680, 24], "fname": "Prims.fst"}]}], "status": "failure"}
{"kind": "response", "query-id": "200", "response": [], "status": "success"}
{"kind": "response", "query-id": "204", "response": [], "status": "success"}
{"kind": "response", "query-id": "205", "response": [{"level": "error", "message": "- Assertion failed\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also (13,15-13,23)\n", "number": 19, "ranges": [{"beg": [13, 8], "end": [13, 14], "fname": ""}, {"beg": [13, 15], "end": [13, 23], "fname": ""}]}], "status": "failure"}
diff --git a/ulib/FStar.Stubs.Errors.Msg.fsti b/ulib/FStar.Stubs.Errors.Msg.fsti
index 667632c77a3..04ebf5dd265 100644
--- a/ulib/FStar.Stubs.Errors.Msg.fsti
+++ b/ulib/FStar.Stubs.Errors.Msg.fsti
@@ -10,7 +10,7 @@ these:
* Error 19 at tests/error-messages/Bug1997.fst(92,19-92,49):
- Assertion failed
- The SMT solver could not prove the query. Use --query_stats for more details.
- - Also see: prims.fst(96,32-96,42)
+ - Also see: Prims.fst(96,32-96,42)
The header is taken from the code and range, and then the documents are rendered
in order.
diff --git a/ulib/Makefile b/ulib/Makefile
index 46c76abc6a8..7b298526804 100644
--- a/ulib/Makefile
+++ b/ulib/Makefile
@@ -44,7 +44,7 @@ clean: clean_checked
$(Q)rm -f .depend.*
$(Q)rm -f *.checked.lax .cache/*.checked.lax
-DOC_FILES=prims.fst FStar.Pervasives.Native.fst FStar.Pervasives.fst \
+DOC_FILES=Prims.fst FStar.Pervasives.Native.fst FStar.Pervasives.fst \
FStar.Squash.fsti FStar.Classical.fsti FStar.BigOps.fsti \
FStar.BitVector.fst FStar.BV.fsti \
FStar.Char.fsti FStar.Date.fsti FStar.DependentMap.fsti \
diff --git a/ulib/prims.fst b/ulib/Prims.fst
similarity index 100%
rename from ulib/prims.fst
rename to ulib/Prims.fst