From f48560f7bc02bef6f920c175b54de09547d96cbd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 15 Oct 2024 07:40:34 -0700 Subject: [PATCH] snap for F* change --- src/ocaml/plugin/generated/Pulse_Checker.ml | 5 +++-- src/ocaml/plugin/generated/Pulse_Checker_Abs.ml | 2 +- src/ocaml/plugin/generated/Pulse_Checker_Match.ml | 2 +- .../plugin/generated/Pulse_Checker_WithLocal.ml | 2 +- .../generated/Pulse_Checker_WithLocalArray.ml | 2 +- src/ocaml/plugin/generated/Pulse_Extract_Main.ml | 10 +++++----- src/ocaml/plugin/generated/Pulse_Syntax_Base.ml | 2 +- src/ocaml/plugin/generated/Pulse_Syntax_Printer.ml | 12 ++++++------ src/ocaml/plugin/generated/Pulse_Typing_Env.ml | 14 +++++++------- 9 files changed, 26 insertions(+), 25 deletions(-) diff --git a/src/ocaml/plugin/generated/Pulse_Checker.ml b/src/ocaml/plugin/generated/Pulse_Checker.ml index 1ded7a041..f7ed3b455 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker.ml @@ -765,7 +765,8 @@ let (trace : (fun msg -> let uu___2 = let uu___3 = - let uu___4 = FStar_Tactics_Unseal.unseal rng in + let uu___4 = + FStarC_Tactics_Unseal.unseal rng in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic @@ -915,7 +916,7 @@ let (maybe_trace : (fun uu___2 -> (fun trace_full_opt -> let uu___2 = - FStar_Tactics_Unseal.unseal + FStarC_Tactics_Unseal.unseal t.Pulse_Syntax_Base.source in Obj.magic (FStar_Tactics_Effect.tac_bind diff --git a/src/ocaml/plugin/generated/Pulse_Checker_Abs.ml b/src/ocaml/plugin/generated/Pulse_Checker_Abs.ml index 115b876c5..923c72315 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_Abs.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_Abs.ml @@ -3594,7 +3594,7 @@ let rec (check_abs_core : = let uu___28 = - FStar_Tactics_Unseal.unseal + FStarC_Tactics_Unseal.unseal binder_attrs in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal diff --git a/src/ocaml/plugin/generated/Pulse_Checker_Match.ml b/src/ocaml/plugin/generated/Pulse_Checker_Match.ml index b0b6cb32d..bd40b1320 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_Match.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_Match.ml @@ -87,7 +87,7 @@ let rec (r_bindings_to_string : (Obj.repr (let uu___ = let uu___1 = - FStar_Tactics_Unseal.unseal + FStarC_Tactics_Unseal.unseal b.FStarC_Reflection_V2_Data.ppname3 in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal diff --git a/src/ocaml/plugin/generated/Pulse_Checker_WithLocal.ml b/src/ocaml/plugin/generated/Pulse_Checker_WithLocal.ml index bb6715826..3e3d81709 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_WithLocal.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_WithLocal.ml @@ -566,7 +566,7 @@ let (check : = let uu___9 = - FStar_Tactics_Unseal.unseal + FStarC_Tactics_Unseal.unseal (binder.Pulse_Syntax_Base.binder_ppname).Pulse_Syntax_Base.name in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal diff --git a/src/ocaml/plugin/generated/Pulse_Checker_WithLocalArray.ml b/src/ocaml/plugin/generated/Pulse_Checker_WithLocalArray.ml index 8882ded14..3baa730b0 100644 --- a/src/ocaml/plugin/generated/Pulse_Checker_WithLocalArray.ml +++ b/src/ocaml/plugin/generated/Pulse_Checker_WithLocalArray.ml @@ -724,7 +724,7 @@ let (check : = let uu___11 = - FStar_Tactics_Unseal.unseal + FStarC_Tactics_Unseal.unseal (binder.Pulse_Syntax_Base.binder_ppname).Pulse_Syntax_Base.name in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal diff --git a/src/ocaml/plugin/generated/Pulse_Extract_Main.ml b/src/ocaml/plugin/generated/Pulse_Extract_Main.ml index d2347753c..c449855d4 100644 --- a/src/ocaml/plugin/generated/Pulse_Extract_Main.ml +++ b/src/ocaml/plugin/generated/Pulse_Extract_Main.ml @@ -108,7 +108,7 @@ let rec (extend_env'_pattern : | Pulse_Syntax_Base.Pat_Var (ppname, sort) -> Obj.magic (Obj.repr - (let uu___ = FStar_Tactics_Unseal.unseal sort in + (let uu___ = FStarC_Tactics_Unseal.unseal sort in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic @@ -226,7 +226,7 @@ let (is_erasable : (Prims.bool, unit) FStar_Tactics_Effect.tac_repr) = fun p -> - let uu___ = FStar_Tactics_Unseal.unseal p.Pulse_Syntax_Base.effect_tag in + let uu___ = FStarC_Tactics_Unseal.unseal p.Pulse_Syntax_Base.effect_tag in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic @@ -359,7 +359,7 @@ let (is_internal_binder : = fun b -> let uu___ = - FStar_Tactics_Unseal.unseal + FStarC_Tactics_Unseal.unseal (b.Pulse_Syntax_Base.binder_ppname).Pulse_Syntax_Base.name in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal @@ -2836,7 +2836,7 @@ let (extract_dv_binder : fun q -> let uu___ = let uu___1 = - FStar_Tactics_Unseal.unseal b.Pulse_Syntax_Base.binder_attrs in + FStarC_Tactics_Unseal.unseal b.Pulse_Syntax_Base.binder_attrs in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic @@ -2963,7 +2963,7 @@ let rec (extract_dv_pattern : | Pulse_Syntax_Base.Pat_Var (ppname, sort) -> Obj.magic (Obj.repr - (let uu___ = FStar_Tactics_Unseal.unseal sort in + (let uu___ = FStarC_Tactics_Unseal.unseal sort in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic diff --git a/src/ocaml/plugin/generated/Pulse_Syntax_Base.ml b/src/ocaml/plugin/generated/Pulse_Syntax_Base.ml index 4047b0531..6505e8d13 100644 --- a/src/ocaml/plugin/generated/Pulse_Syntax_Base.ml +++ b/src/ocaml/plugin/generated/Pulse_Syntax_Base.ml @@ -905,7 +905,7 @@ let (ppname_for_uvar : fun p -> let uu___ = let uu___1 = - let uu___2 = FStar_Tactics_Unseal.unseal p.name in + let uu___2 = FStarC_Tactics_Unseal.unseal p.name in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic diff --git a/src/ocaml/plugin/generated/Pulse_Syntax_Printer.ml b/src/ocaml/plugin/generated/Pulse_Syntax_Printer.ml index 8a58c4ddc..f85c0f5dd 100644 --- a/src/ocaml/plugin/generated/Pulse_Syntax_Printer.ml +++ b/src/ocaml/plugin/generated/Pulse_Syntax_Printer.ml @@ -87,7 +87,7 @@ let rec (binder_to_string_paren : (fun uu___1 -> let uu___2 = let uu___3 = - FStar_Tactics_Unseal.unseal + FStarC_Tactics_Unseal.unseal (b.Pulse_Syntax_Base.binder_ppname).Pulse_Syntax_Base.name in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal @@ -106,7 +106,7 @@ let rec (binder_to_string_paren : let uu___5 = let uu___6 = let uu___7 = - FStar_Tactics_Unseal.unseal + FStarC_Tactics_Unseal.unseal b.Pulse_Syntax_Base.binder_attrs in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal @@ -853,7 +853,7 @@ let rec (binder_to_doc : let uu___ = let uu___1 = let uu___2 = - FStar_Tactics_Unseal.unseal + FStarC_Tactics_Unseal.unseal (b.Pulse_Syntax_Base.binder_ppname).Pulse_Syntax_Base.name in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal @@ -1658,7 +1658,7 @@ let (binder_to_string : (fun uu___1 -> let uu___2 = let uu___3 = - FStar_Tactics_Unseal.unseal + FStarC_Tactics_Unseal.unseal (b.Pulse_Syntax_Base.binder_ppname).Pulse_Syntax_Base.name in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal @@ -1677,7 +1677,7 @@ let (binder_to_string : let uu___5 = let uu___6 = let uu___7 = - FStar_Tactics_Unseal.unseal + FStarC_Tactics_Unseal.unseal b.Pulse_Syntax_Base.binder_attrs in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal @@ -5475,7 +5475,7 @@ and (pattern_to_string : (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> ""))) | Pulse_Syntax_Base.Pat_Var (x, uu___) -> - Obj.magic (Obj.repr (FStar_Tactics_Unseal.unseal x)) + Obj.magic (Obj.repr (FStarC_Tactics_Unseal.unseal x)) | Pulse_Syntax_Base.Pat_Dot_Term (FStar_Pervasives_Native.None) -> Obj.magic (Obj.repr (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> ""))) diff --git a/src/ocaml/plugin/generated/Pulse_Typing_Env.ml b/src/ocaml/plugin/generated/Pulse_Typing_Env.ml index 13a8f18da..798a83948 100644 --- a/src/ocaml/plugin/generated/Pulse_Typing_Env.ml +++ b/src/ocaml/plugin/generated/Pulse_Typing_Env.ml @@ -289,7 +289,7 @@ let (get_context : env -> Pulse_RuntimeUtils.context) = fun g -> g.ctxt let (range_of_env : env -> (Pulse_Syntax_Base.range, unit) FStar_Tactics_Effect.tac_repr) = fun g -> - let uu___ = FStar_Tactics_Unseal.unseal g.ctxt in + let uu___ = FStarC_Tactics_Unseal.unseal g.ctxt in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic @@ -429,7 +429,7 @@ let (ctx_to_string : let (ctxt_to_list : env -> (Prims.string Prims.list, unit) FStar_Tactics_Effect.tac_repr) = fun g -> - let uu___ = FStar_Tactics_Unseal.unseal g.ctxt in + let uu___ = FStarC_Tactics_Unseal.unseal g.ctxt in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic @@ -446,7 +446,7 @@ let (ctxt_to_list : let (print_context : env -> (Prims.string, unit) FStar_Tactics_Effect.tac_repr) = fun g -> - let uu___ = FStar_Tactics_Unseal.unseal g.ctxt in + let uu___ = FStarC_Tactics_Unseal.unseal g.ctxt in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic @@ -541,7 +541,7 @@ let (print_issue : (fun range_opt_to_string -> let uu___1 = let uu___2 = - let uu___3 = FStar_Tactics_Unseal.unseal (get_context g) in + let uu___3 = FStarC_Tactics_Unseal.unseal (get_context g) in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic @@ -791,7 +791,7 @@ let (env_to_string : let uu___6 = let uu___7 = let uu___8 = - FStar_Tactics_Unseal.unseal + FStarC_Tactics_Unseal.unseal x.Pulse_Syntax_Base.name in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal @@ -986,7 +986,7 @@ let (env_to_doc' : let uu___3 = let uu___4 = let uu___5 = - FStar_Tactics_Unseal.unseal + FStarC_Tactics_Unseal.unseal x.Pulse_Syntax_Base.name in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal @@ -1178,7 +1178,7 @@ let (env_to_doc' : = let uu___7 = - FStar_Tactics_Unseal.unseal + FStarC_Tactics_Unseal.unseal x1.Pulse_Syntax_Base.name in FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal