From a6e57b4c4e4d6b26d64070bbd5f31687c667dc21 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Mon, 27 Nov 2023 14:27:21 -0800
Subject: [PATCH] snap

---
 .../generated/FStar_Class_HasRange.ml         | 17 ++++++++
 .../generated/FStar_Syntax_Syntax.ml          | 41 ++++++++++++++++++-
 .../generated/FStar_Tactics_V2_Basic.ml       |  3 +-
 3 files changed, 59 insertions(+), 2 deletions(-)
 create mode 100644 ocaml/fstar-lib/generated/FStar_Class_HasRange.ml

diff --git a/ocaml/fstar-lib/generated/FStar_Class_HasRange.ml b/ocaml/fstar-lib/generated/FStar_Class_HasRange.ml
new file mode 100644
index 00000000000..359765f9910
--- /dev/null
+++ b/ocaml/fstar-lib/generated/FStar_Class_HasRange.ml
@@ -0,0 +1,17 @@
+open Prims
+type 'a hasRange =
+  {
+  pos: 'a -> FStar_Compiler_Range_Type.range ;
+  setPos: FStar_Compiler_Range_Type.range -> 'a -> 'a }
+let __proj__MkhasRange__item__pos :
+  'a . 'a hasRange -> 'a -> FStar_Compiler_Range_Type.range =
+  fun projectee -> match projectee with | { pos; setPos;_} -> pos
+let __proj__MkhasRange__item__setPos :
+  'a . 'a hasRange -> FStar_Compiler_Range_Type.range -> 'a -> 'a =
+  fun projectee -> match projectee with | { pos; setPos;_} -> setPos
+let pos : 'a . 'a hasRange -> 'a -> FStar_Compiler_Range_Type.range =
+  fun projectee -> match projectee with | { pos = pos1; setPos;_} -> pos1
+let setPos : 'a . 'a hasRange -> FStar_Compiler_Range_Type.range -> 'a -> 'a
+  =
+  fun projectee ->
+    match projectee with | { pos = pos1; setPos = setPos1;_} -> setPos1
\ No newline at end of file
diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml
index b2512c01fc9..49752d36f7a 100644
--- a/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml
+++ b/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml
@@ -2764,4 +2764,43 @@ let (t_sealed_of : term -> term) =
 let (unit_const_with_range : FStar_Compiler_Range_Type.range -> term) =
   fun r -> mk (Tm_constant FStar_Const.Const_unit) r
 let (unit_const : term) =
-  unit_const_with_range FStar_Compiler_Range_Type.dummyRange
\ No newline at end of file
+  unit_const_with_range FStar_Compiler_Range_Type.dummyRange
+let has_range_syntax : 'a . unit -> 'a syntax FStar_Class_HasRange.hasRange =
+  fun uu___ ->
+    (fun uu___ ->
+       Obj.magic
+         {
+           FStar_Class_HasRange.pos = (fun t -> t.pos);
+           FStar_Class_HasRange.setPos =
+             (fun r ->
+                fun t ->
+                  {
+                    n = (t.n);
+                    pos = r;
+                    vars = (t.vars);
+                    hash_code = (t.hash_code)
+                  })
+         }) uu___
+let has_range_withinfo :
+  'a . unit -> 'a withinfo_t FStar_Class_HasRange.hasRange =
+  fun uu___ ->
+    {
+      FStar_Class_HasRange.pos = (fun t -> t.p);
+      FStar_Class_HasRange.setPos = (fun r -> fun t -> { v = (t.v); p = r })
+    }
+let (has_range_sigelt : sigelt FStar_Class_HasRange.hasRange) =
+  {
+    FStar_Class_HasRange.pos = (fun t -> t.sigrng);
+    FStar_Class_HasRange.setPos =
+      (fun r ->
+         fun t ->
+           {
+             sigel = (t.sigel);
+             sigrng = r;
+             sigquals = (t.sigquals);
+             sigmeta = (t.sigmeta);
+             sigattrs = (t.sigattrs);
+             sigopens_and_abbrevs = (t.sigopens_and_abbrevs);
+             sigopts = (t.sigopts)
+           })
+  }
\ No newline at end of file
diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml
index 5a8104298ce..0d684bc4fc1 100644
--- a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml
+++ b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml
@@ -1246,7 +1246,8 @@ let (tadmit_t : FStar_Syntax_Syntax.term -> unit FStar_Tactics_Monad.tac) =
              (fun g ->
                 (let uu___2 =
                    let uu___3 = FStar_Tactics_Types.goal_type g in
-                   uu___3.FStar_Syntax_Syntax.pos in
+                   FStar_Class_HasRange.pos
+                     (FStar_Syntax_Syntax.has_range_syntax ()) uu___3 in
                  let uu___3 =
                    let uu___4 =
                      let uu___5 =