From ffc0adb32f8dcf525f0fbb8ee4c4e7b0b5a5b675 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 15 Sep 2024 19:56:23 -0700 Subject: [PATCH] snap+parser update after F* changes --- src/ocaml/plugin/FStar_Parser_Parse.mly | 7 +- .../plugin/generated/Pulse_Checker_Abs.ml | 18 +-- .../Pulse_Checker_AssertWithBinders.ml | 4 +- .../plugin/generated/Pulse_Checker_Bind.ml | 2 +- .../plugin/generated/Pulse_Checker_Comp.ml | 2 +- .../plugin/generated/Pulse_Checker_Exists.ml | 6 +- .../plugin/generated/Pulse_Checker_Match.ml | 20 +-- .../plugin/generated/Pulse_Checker_Prover.ml | 4 +- .../Pulse_Checker_Prover_IntroPure.ml | 4 +- .../Pulse_Checker_Prover_Match_Comb.ml | 10 +- .../plugin/generated/Pulse_Checker_Pure.ml | 8 +- .../plugin/generated/Pulse_Checker_Return.ml | 2 +- .../plugin/generated/Pulse_Checker_STApp.ml | 8 +- .../plugin/generated/Pulse_Checker_While.ml | 6 +- .../generated/Pulse_Checker_WithLocal.ml | 2 +- .../generated/Pulse_Checker_WithLocalArray.ml | 4 +- .../plugin/generated/Pulse_Extract_Main.ml | 22 +-- src/ocaml/plugin/generated/Pulse_Main.ml | 4 +- src/ocaml/plugin/generated/Pulse_Recursion.ml | 2 +- src/ocaml/plugin/generated/Pulse_Show.ml | 140 +++++++++--------- .../plugin/generated/Pulse_Syntax_Base.ml | 2 +- .../plugin/generated/Pulse_Syntax_Printer.ml | 58 ++++---- src/ocaml/plugin/generated/Pulse_Typing.ml | 2 +- .../generated/Pulse_Typing_Combinators.ml | 2 +- .../plugin/generated/Pulse_Typing_Env.ml | 8 +- .../plugin/generated/Pulse_Typing_Printer.ml | 6 +- 26 files changed, 179 insertions(+), 174 deletions(-) diff --git a/src/ocaml/plugin/FStar_Parser_Parse.mly b/src/ocaml/plugin/FStar_Parser_Parse.mly index 4eb4587ed..be1f06e7a 100644 --- a/src/ocaml/plugin/FStar_Parser_Parse.mly +++ b/src/ocaml/plugin/FStar_Parser_Parse.mly @@ -108,7 +108,8 @@ let parse_use_lang_blob (extension_name:string) %token ASSUME NEW LOGIC ATTRIBUTES %token IRREDUCIBLE UNFOLDABLE INLINE OPAQUE UNFOLD INLINE_FOR_EXTRACTION %token NOEXTRACT -%token NOEQUALITY UNOPTEQUALITY PRAGMA_SET_OPTIONS PRAGMA_RESET_OPTIONS PRAGMA_PUSH_OPTIONS PRAGMA_POP_OPTIONS PRAGMA_RESTART_SOLVER PRAGMA_PRINT_EFFECTS_GRAPH +%token NOEQUALITY UNOPTEQUALITY +%token PRAGMA_SHOW_OPTIONS PRAGMA_SET_OPTIONS PRAGMA_RESET_OPTIONS PRAGMA_PUSH_OPTIONS PRAGMA_POP_OPTIONS PRAGMA_RESTART_SOLVER PRAGMA_PRINT_EFFECTS_GRAPH %token TYP_APP_LESS TYP_APP_GREATER SUBTYPE EQUALTYPE SUBKIND BY %token AND ASSERT SYNTH BEGIN ELSE END %token EXCEPTION FALSE FUN FUNCTION IF IN MODULE DEFAULT @@ -221,6 +222,8 @@ startOfNextDeclToken: | b=USE_LANG_BLOB { let _, _, _, snap = b in Some snap } pragmaStartToken: + | PRAGMA_SHOW_OPTIONS + { () } | PRAGMA_SET_OPTIONS { () } | PRAGMA_RESET_OPTIONS @@ -239,6 +242,8 @@ pragmaStartToken: /******************************************************************************/ pragma: + | PRAGMA_SHOW_OPTIONS + { ShowOptions } | PRAGMA_SET_OPTIONS s=string { SetOptions s } | PRAGMA_RESET_OPTIONS s_opt=string? diff --git a/src/ocaml/plugin/generated/Pulse_Checker_Abs.ml b/src/ocaml/plugin/generated/Pulse_Checker_Abs.ml index 7cd0471dc..5d4971eb6 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_Abs.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_Abs.ml @@ -433,7 +433,7 @@ let rec (arrow_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)) @@ -907,7 +907,7 @@ let rec (rebuild_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)) @@ -1014,7 +1014,7 @@ let rec (rebuild_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)) @@ -1088,7 +1088,7 @@ let rec (rebuild_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)) @@ -1203,7 +1203,7 @@ let rec (rebuild_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)) @@ -1267,7 +1267,7 @@ let rec (rebuild_abs : (Prims.of_int (166)) (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___4) @@ -1334,7 +1334,7 @@ let (preprocess_abs : (Prims.of_int (173)) (Prims.of_int (87))))) (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) @@ -1425,7 +1425,7 @@ let (preprocess_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)) @@ -3799,7 +3799,7 @@ let rec (check_abs_core : (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/src/ocaml/plugin/generated/Pulse_Checker_AssertWithBinders.ml b/src/ocaml/plugin/generated/Pulse_Checker_AssertWithBinders.ml index db7d37b54..1c1e2e085 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_AssertWithBinders.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_AssertWithBinders.ml @@ -745,7 +745,7 @@ let (unfold_head : (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)) @@ -889,7 +889,7 @@ let (check_unfoldable : (Prims.of_int (189)) (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___2) diff --git a/src/ocaml/plugin/generated/Pulse_Checker_Bind.ml b/src/ocaml/plugin/generated/Pulse_Checker_Bind.ml index 6bcd854d4..e306f1701 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_Bind.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_Bind.ml @@ -504,7 +504,7 @@ let (check_bind : (Prims.of_int (65))))) (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)) diff --git a/src/ocaml/plugin/generated/Pulse_Checker_Comp.ml b/src/ocaml/plugin/generated/Pulse_Checker_Comp.ml index 83e5de757..be7b69d8b 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_Comp.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_Comp.ml @@ -333,7 +333,7 @@ let (check : (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/src/ocaml/plugin/generated/Pulse_Checker_Exists.ml b/src/ocaml/plugin/generated/Pulse_Checker_Exists.ml index 5aeeb6de0..221ec51d4 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_Exists.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_Exists.ml @@ -219,7 +219,7 @@ let (check_elim_exists : (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)) @@ -422,7 +422,7 @@ let (check_elim_exists : (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 (check_intro_exists : (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/src/ocaml/plugin/generated/Pulse_Checker_Match.ml b/src/ocaml/plugin/generated/Pulse_Checker_Match.ml index 9888ecbe7..c5f721fee 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_Match.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_Match.ml @@ -120,7 +120,7 @@ let rec (r_bindings_to_string : (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)) @@ -141,7 +141,7 @@ let rec (r_bindings_to_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)) @@ -162,7 +162,7 @@ let rec (r_bindings_to_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)) @@ -186,7 +186,7 @@ let rec (r_bindings_to_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)) @@ -207,7 +207,7 @@ let rec (r_bindings_to_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)) @@ -244,7 +244,7 @@ let rec (r_bindings_to_string : (Prims.of_int (116))))) (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)) @@ -282,7 +282,7 @@ let rec (bindings_to_string : (Prims.of_int (212)) (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)) (Prims.of_int (31))))) (Obj.magic uu___3) @@ -297,7 +297,7 @@ let rec (bindings_to_string : (Prims.of_int (212)) (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) @@ -312,7 +312,7 @@ let rec (bindings_to_string : (Prims.of_int (212)) (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___1) @@ -349,7 +349,7 @@ let rec (bindings_to_string : (Prims.of_int (109))))) (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)) diff --git a/src/ocaml/plugin/generated/Pulse_Checker_Prover.ml b/src/ocaml/plugin/generated/Pulse_Checker_Prover.ml index 68c915ab5..13558eca0 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_Prover.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_Prover.ml @@ -330,7 +330,7 @@ let rec (prove_pures : (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)) @@ -1133,7 +1133,7 @@ let rec (prover_iteration_loop : (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/src/ocaml/plugin/generated/Pulse_Checker_Prover_IntroPure.ml b/src/ocaml/plugin/generated/Pulse_Checker_Prover_IntroPure.ml index 15d9cf7f1..546b62545 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_Prover_IntroPure.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_Prover_IntroPure.ml @@ -421,7 +421,7 @@ let (is_uvar_implication : pure_uv_heuristic_t) = (Prims.of_int (127)) (Prims.of_int (89))))) (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 -> @@ -516,7 +516,7 @@ let (is_uvar_implication : pure_uv_heuristic_t) = (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/src/ocaml/plugin/generated/Pulse_Checker_Prover_Match_Comb.ml b/src/ocaml/plugin/generated/Pulse_Checker_Prover_Match_Comb.ml index f2de6b3a8..fa8886850 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_Prover_Match_Comb.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_Prover_Match_Comb.ml @@ -1782,7 +1782,7 @@ let rec (match_f_nn : (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)) @@ -1809,7 +1809,7 @@ let rec (match_f_nn : (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)) @@ -1971,7 +1971,7 @@ let rec (match_f_nn : (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)) @@ -2064,7 +2064,7 @@ let rec (match_f_nn : (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)) @@ -2155,7 +2155,7 @@ let rec (match_f_nn : (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/src/ocaml/plugin/generated/Pulse_Checker_Pure.ml b/src/ocaml/plugin/generated/Pulse_Checker_Pure.ml index 2539c5725..411359fb0 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_Pure.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_Pure.ml @@ -62,7 +62,7 @@ let (debug : (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)) @@ -84,7 +84,7 @@ let (debug : (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)) @@ -1153,7 +1153,7 @@ let (rtb_instantiate_implicits : (Prims.of_int (93)) (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___4) @@ -1302,7 +1302,7 @@ let (rtb_instantiate_implicits : (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/src/ocaml/plugin/generated/Pulse_Checker_Return.ml b/src/ocaml/plugin/generated/Pulse_Checker_Return.ml index ea29087a3..3740b5ed0 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_Return.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_Return.ml @@ -895,7 +895,7 @@ let (check_core : (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/src/ocaml/plugin/generated/Pulse_Checker_STApp.ml b/src/ocaml/plugin/generated/Pulse_Checker_STApp.ml index 1225d9cea..67c871404 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_STApp.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_STApp.ml @@ -408,7 +408,7 @@ let rec (intro_uvars_for_logical_implicits : (Prims.of_int (90)) (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___3) @@ -618,7 +618,7 @@ let (instantiate_implicits : (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)) @@ -1226,7 +1226,7 @@ let (apply_impure_function : (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)) @@ -1859,7 +1859,7 @@ let (apply_impure_function : (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/src/ocaml/plugin/generated/Pulse_Checker_While.ml b/src/ocaml/plugin/generated/Pulse_Checker_While.ml index 5938d03c3..94bd28a18 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_While.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_While.ml @@ -188,7 +188,7 @@ let (check : (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)) @@ -344,7 +344,7 @@ let (check : (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)) @@ -858,7 +858,7 @@ let (check : (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/src/ocaml/plugin/generated/Pulse_Checker_WithLocal.ml b/src/ocaml/plugin/generated/Pulse_Checker_WithLocal.ml index 0e035ce7f..dd1daed27 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_WithLocal.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_WithLocal.ml @@ -580,7 +580,7 @@ let (check : (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/src/ocaml/plugin/generated/Pulse_Checker_WithLocalArray.ml b/src/ocaml/plugin/generated/Pulse_Checker_WithLocalArray.ml index f15434a58..6b420f7ca 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_WithLocalArray.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_WithLocalArray.ml @@ -347,7 +347,7 @@ let (check : (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)) @@ -738,7 +738,7 @@ let (check : (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/src/ocaml/plugin/generated/Pulse_Extract_Main.ml b/src/ocaml/plugin/generated/Pulse_Extract_Main.ml index 601756604..7b06b6518 100644 --- a/src/ocaml/plugin/generated/Pulse_Extract_Main.ml +++ b/src/ocaml/plugin/generated/Pulse_Extract_Main.ml @@ -917,7 +917,7 @@ let (maybe_unfold_head : (Prims.of_int (149)) (Prims.of_int (88))))) (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 -> @@ -1079,7 +1079,7 @@ let (maybe_unfold_head : (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)) @@ -1140,7 +1140,7 @@ let (maybe_unfold_head : (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)) @@ -1356,7 +1356,7 @@ let (maybe_inline : (Prims.of_int (214)) (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___2) (fun uu___3 -> @@ -1505,7 +1505,7 @@ let (maybe_inline : (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)) @@ -2214,7 +2214,7 @@ let (maybe_inline : (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)) @@ -5449,7 +5449,7 @@ let rec (extract : (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)) @@ -6263,7 +6263,7 @@ let rec (extract : (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)) @@ -7094,7 +7094,7 @@ let rec (generalize : (Prims.of_int (700)) (Prims.of_int (83))))) (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 -> @@ -8485,7 +8485,7 @@ let (extract_pulse : (Prims.of_int (824)) (Prims.of_int (82))))) (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) @@ -9266,7 +9266,7 @@ let (extract_pulse_sig : (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/src/ocaml/plugin/generated/Pulse_Main.ml b/src/ocaml/plugin/generated/Pulse_Main.ml index 7f8958c6f..14d26e414 100644 --- a/src/ocaml/plugin/generated/Pulse_Main.ml +++ b/src/ocaml/plugin/generated/Pulse_Main.ml @@ -419,7 +419,7 @@ let (check_fndefn : (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)) @@ -2161,7 +2161,7 @@ let (main' : (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/src/ocaml/plugin/generated/Pulse_Recursion.ml b/src/ocaml/plugin/generated/Pulse_Recursion.ml index 073722ffd..00397646e 100644 --- a/src/ocaml/plugin/generated/Pulse_Recursion.ml +++ b/src/ocaml/plugin/generated/Pulse_Recursion.ml @@ -322,7 +322,7 @@ let (add_knot : (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/src/ocaml/plugin/generated/Pulse_Show.ml b/src/ocaml/plugin/generated/Pulse_Show.ml index 929ee4dce..89f940eb6 100644 --- a/src/ocaml/plugin/generated/Pulse_Show.ml +++ b/src/ocaml/plugin/generated/Pulse_Show.ml @@ -71,7 +71,7 @@ let tac_showable_option : (Prims.of_int (43)) (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) @@ -238,7 +238,7 @@ let (tac_showable_post_hint_t : Pulse_Typing.post_hint_t tac_showable) = (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)) @@ -267,7 +267,7 @@ let (tac_showable_post_hint_t : Pulse_Typing.post_hint_t tac_showable) = (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)) @@ -296,7 +296,7 @@ let (tac_showable_post_hint_t : Pulse_Typing.post_hint_t tac_showable) = (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)) @@ -328,7 +328,7 @@ let (tac_showable_post_hint_t : Pulse_Typing.post_hint_t tac_showable) = 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)) @@ -360,7 +360,7 @@ let (tac_showable_post_hint_t : Pulse_Typing.post_hint_t tac_showable) = (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)) @@ -384,7 +384,7 @@ let (tac_showable_post_hint_t : Pulse_Typing.post_hint_t tac_showable) = (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)) @@ -408,7 +408,7 @@ let (tac_showable_post_hint_t : Pulse_Typing.post_hint_t tac_showable) = (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)) @@ -433,7 +433,7 @@ let (tac_showable_post_hint_t : Pulse_Typing.post_hint_t tac_showable) = (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)) @@ -456,7 +456,7 @@ let (tac_showable_post_hint_t : Pulse_Typing.post_hint_t tac_showable) = (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 (tac_showable_post_hint_t : Pulse_Typing.post_hint_t tac_showable) = (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)) @@ -498,7 +498,7 @@ let (tac_showable_post_hint_t : Pulse_Typing.post_hint_t tac_showable) = (Prims.of_int (84)) (Prims.of_int (7))))) (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) @@ -514,7 +514,7 @@ let (tac_showable_post_hint_t : Pulse_Typing.post_hint_t tac_showable) = (Prims.of_int (84)) (Prims.of_int (7))))) (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) @@ -530,7 +530,7 @@ let (tac_showable_post_hint_t : Pulse_Typing.post_hint_t tac_showable) = (Prims.of_int (84)) (Prims.of_int (7))))) (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) @@ -546,7 +546,7 @@ let (tac_showable_post_hint_t : Pulse_Typing.post_hint_t tac_showable) = (Prims.of_int (7))))) (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 -> @@ -559,7 +559,7 @@ let (tac_showable_post_hint_t : Pulse_Typing.post_hint_t tac_showable) = (Prims.of_int (6)) (Prims.of_int (84)) (Prims.of_int (7))))) (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 -> @@ -608,7 +608,7 @@ let tac_showable_tuple2 : (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)) @@ -627,7 +627,7 @@ let tac_showable_tuple2 : (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)) @@ -647,7 +647,7 @@ let tac_showable_tuple2 : (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)) @@ -665,7 +665,7 @@ let tac_showable_tuple2 : (Prims.of_int (96)) (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) @@ -740,7 +740,7 @@ let tac_showable_tuple3 : (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)) @@ -763,7 +763,7 @@ let tac_showable_tuple3 : (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)) @@ -787,7 +787,7 @@ let tac_showable_tuple3 : (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)) @@ -808,7 +808,7 @@ let tac_showable_tuple3 : (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)) @@ -830,7 +830,7 @@ let tac_showable_tuple3 : (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)) @@ -849,7 +849,7 @@ let tac_showable_tuple3 : (Prims.of_int (100)) (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___4) @@ -951,7 +951,7 @@ let tac_showable_tuple4 : (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 tac_showable_tuple4 : (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)) @@ -1004,7 +1004,7 @@ let tac_showable_tuple4 : (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)) @@ -1031,7 +1031,7 @@ let tac_showable_tuple4 : (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)) @@ -1055,7 +1055,7 @@ let tac_showable_tuple4 : (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)) @@ -1077,7 +1077,7 @@ let tac_showable_tuple4 : (Prims.of_int (96))))) (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)) @@ -1099,7 +1099,7 @@ let tac_showable_tuple4 : (Prims.of_int (96))))) (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)) @@ -1118,7 +1118,7 @@ let tac_showable_tuple4 : (Prims.of_int (104)) (Prims.of_int (96))))) (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) @@ -1254,7 +1254,7 @@ let tac_showable_tuple5 : (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)) @@ -1283,7 +1283,7 @@ let tac_showable_tuple5 : (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)) @@ -1313,7 +1313,7 @@ let tac_showable_tuple5 : (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)) @@ -1343,7 +1343,7 @@ let tac_showable_tuple5 : (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)) @@ -1373,7 +1373,7 @@ let tac_showable_tuple5 : (Obj.magic ( FStar_Range.mk_range - "prims.fst" + "Prims.fst" (Prims.of_int (611)) (Prims.of_int (19)) (Prims.of_int (611)) @@ -1401,7 +1401,7 @@ let tac_showable_tuple5 : (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)) @@ -1425,7 +1425,7 @@ let tac_showable_tuple5 : (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)) @@ -1448,7 +1448,7 @@ let tac_showable_tuple5 : (Prims.of_int (115))))) (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)) @@ -1470,7 +1470,7 @@ let tac_showable_tuple5 : (Prims.of_int (115))))) (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)) @@ -1489,7 +1489,7 @@ let tac_showable_tuple5 : (Prims.of_int (108)) (Prims.of_int (115))))) (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) @@ -1668,7 +1668,7 @@ let tac_showable_tuple6 : (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)) @@ -1697,7 +1697,7 @@ let tac_showable_tuple6 : (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)) @@ -1727,7 +1727,7 @@ let tac_showable_tuple6 : (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)) @@ -1757,7 +1757,7 @@ let tac_showable_tuple6 : (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)) @@ -1787,7 +1787,7 @@ let tac_showable_tuple6 : (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)) @@ -1817,7 +1817,7 @@ let tac_showable_tuple6 : (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)) @@ -1847,7 +1847,7 @@ let tac_showable_tuple6 : (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)) @@ -1876,7 +1876,7 @@ let tac_showable_tuple6 : (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)) @@ -1900,7 +1900,7 @@ let tac_showable_tuple6 : (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)) @@ -1924,7 +1924,7 @@ let tac_showable_tuple6 : (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)) @@ -1947,7 +1947,7 @@ let tac_showable_tuple6 : (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)) @@ -1966,7 +1966,7 @@ let tac_showable_tuple6 : (Prims.of_int (112)) (Prims.of_int (134))))) (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) @@ -2181,7 +2181,7 @@ let tac_showable_tuple7 : (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)) @@ -2210,7 +2210,7 @@ let tac_showable_tuple7 : (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)) @@ -2240,7 +2240,7 @@ let tac_showable_tuple7 : (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)) @@ -2270,7 +2270,7 @@ let tac_showable_tuple7 : (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)) @@ -2300,7 +2300,7 @@ let tac_showable_tuple7 : (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)) @@ -2330,7 +2330,7 @@ let tac_showable_tuple7 : (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)) @@ -2360,7 +2360,7 @@ let tac_showable_tuple7 : (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)) @@ -2392,7 +2392,7 @@ let tac_showable_tuple7 : ( Obj.magic (FStar_Range.mk_range - "prims.fst" + "Prims.fst" (Prims.of_int (611)) (Prims.of_int (19)) (Prims.of_int (611)) @@ -2421,7 +2421,7 @@ let tac_showable_tuple7 : (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)) @@ -2451,7 +2451,7 @@ let tac_showable_tuple7 : (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)) @@ -2475,7 +2475,7 @@ let tac_showable_tuple7 : (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)) @@ -2500,7 +2500,7 @@ let tac_showable_tuple7 : (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)) @@ -2523,7 +2523,7 @@ let tac_showable_tuple7 : (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)) @@ -2544,7 +2544,7 @@ let tac_showable_tuple7 : (Prims.of_int (153))))) (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)) diff --git a/src/ocaml/plugin/generated/Pulse_Syntax_Base.ml b/src/ocaml/plugin/generated/Pulse_Syntax_Base.ml index 23f6577bb..f82867bea 100644 --- a/src/ocaml/plugin/generated/Pulse_Syntax_Base.ml +++ b/src/ocaml/plugin/generated/Pulse_Syntax_Base.ml @@ -907,7 +907,7 @@ let (ppname_for_uvar : (Prims.of_int (416)) (Prims.of_int (47))))) (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/ocaml/plugin/generated/Pulse_Syntax_Printer.ml b/src/ocaml/plugin/generated/Pulse_Syntax_Printer.ml index 8adfeb02c..5ee49e63e 100644 --- a/src/ocaml/plugin/generated/Pulse_Syntax_Printer.ml +++ b/src/ocaml/plugin/generated/Pulse_Syntax_Printer.ml @@ -172,7 +172,7 @@ let rec (binder_to_string_paren : (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)) @@ -268,7 +268,7 @@ and (term_to_string' : (Prims.of_int (91)) (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___) @@ -1743,7 +1743,7 @@ let (binder_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)) @@ -1849,7 +1849,7 @@ let (effect_annot_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___1) @@ -1870,7 +1870,7 @@ let (effect_annot_to_string : (Prims.of_int (222)) (Prims.of_int (81))))) (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) @@ -1892,7 +1892,7 @@ let (effect_annot_to_string : (Prims.of_int (223)) (Prims.of_int (97))))) (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) @@ -1917,7 +1917,7 @@ let (comp_to_string : (Prims.of_int (229)) (Prims.of_int (41))))) (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 -> @@ -2429,7 +2429,7 @@ let rec (st_term_to_string' : (Prims.of_int (268)) (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___1) @@ -2883,7 +2883,7 @@ let rec (st_term_to_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)) @@ -3507,7 +3507,7 @@ let rec (st_term_to_string' : (Prims.of_int (328)) (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___) @@ -3530,7 +3530,7 @@ let rec (st_term_to_string' : (Prims.of_int (332)) (Prims.of_int (26))))) (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___) @@ -4645,7 +4645,7 @@ let rec (st_term_to_string' : (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)) @@ -4797,7 +4797,7 @@ let rec (st_term_to_string' : (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)) @@ -5113,7 +5113,7 @@ let rec (st_term_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)) @@ -5178,7 +5178,7 @@ let rec (st_term_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)) @@ -5396,7 +5396,7 @@ let rec (st_term_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)) @@ -5724,7 +5724,7 @@ and (branches_to_string : (Prims.of_int (55))))) (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)) @@ -5861,7 +5861,7 @@ and (pattern_to_string : (Prims.of_int (454)) (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___) @@ -5957,7 +5957,7 @@ let (tag_of_comp : (Prims.of_int (509)) (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___1) @@ -6105,7 +6105,7 @@ let (decl_to_string : (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)) @@ -6123,7 +6123,7 @@ let (decl_to_string : (Prims.of_int (571)) (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___9) @@ -6141,7 +6141,7 @@ let (decl_to_string : (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)) @@ -6159,7 +6159,7 @@ let (decl_to_string : (Prims.of_int (571)) (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___5) (fun uu___6 -> @@ -6173,7 +6173,7 @@ let (decl_to_string : (Prims.of_int (571)) (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___4) (fun uu___5 -> @@ -6191,7 +6191,7 @@ let (decl_to_string : (Prims.of_int (571)) (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___3) (fun uu___4 -> @@ -6206,7 +6206,7 @@ let (decl_to_string : (Prims.of_int (571)) (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___2) (fun uu___3 -> @@ -6247,7 +6247,7 @@ let (decl_to_string : (Prims.of_int (575)) (Prims.of_int (70))))) (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 -> @@ -6261,7 +6261,7 @@ let (decl_to_string : (Prims.of_int (575)) (Prims.of_int (70))))) (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 -> @@ -6279,7 +6279,7 @@ let (decl_to_string : (Prims.of_int (575)) (Prims.of_int (70))))) (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 -> diff --git a/src/ocaml/plugin/generated/Pulse_Typing.ml b/src/ocaml/plugin/generated/Pulse_Typing.ml index b0e470a65..faadcdb42 100644 --- a/src/ocaml/plugin/generated/Pulse_Typing.ml +++ b/src/ocaml/plugin/generated/Pulse_Typing.ml @@ -27,7 +27,7 @@ let (debug_log : (Prims.of_int (35)) (Prims.of_int (63))))) (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) diff --git a/src/ocaml/plugin/generated/Pulse_Typing_Combinators.ml b/src/ocaml/plugin/generated/Pulse_Typing_Combinators.ml index 2c40856f0..aa9b61d83 100644 --- a/src/ocaml/plugin/generated/Pulse_Typing_Combinators.ml +++ b/src/ocaml/plugin/generated/Pulse_Typing_Combinators.ml @@ -3471,7 +3471,7 @@ let (bind_res_and_post_typing : (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/src/ocaml/plugin/generated/Pulse_Typing_Env.ml b/src/ocaml/plugin/generated/Pulse_Typing_Env.ml index 1eae801f1..350b2b563 100644 --- a/src/ocaml/plugin/generated/Pulse_Typing_Env.ml +++ b/src/ocaml/plugin/generated/Pulse_Typing_Env.ml @@ -381,7 +381,7 @@ let (ctxt_elt_to_string : (Prims.of_int (323)) (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)) (Prims.of_int (31))))) (Obj.magic uu___) @@ -431,7 +431,7 @@ let (ctx_to_string : (Prims.of_int (329)) (Prims.of_int (93))))) (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) @@ -507,7 +507,7 @@ let (print_context : (Prims.of_int (340)) (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___2) @@ -1011,7 +1011,7 @@ let (env_to_doc' : (Prims.of_int (379)) (Prims.of_int (39))))) (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) diff --git a/src/ocaml/plugin/generated/Pulse_Typing_Printer.ml b/src/ocaml/plugin/generated/Pulse_Typing_Printer.ml index 2d517f8d5..9e0dc2265 100644 --- a/src/ocaml/plugin/generated/Pulse_Typing_Printer.ml +++ b/src/ocaml/plugin/generated/Pulse_Typing_Printer.ml @@ -38,7 +38,7 @@ let rec (print_st_typing : (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)) @@ -82,7 +82,7 @@ let rec (print_st_typing : (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)) @@ -289,7 +289,7 @@ let rec (print_st_typing : (Prims.of_int (28))))) (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))