From 93d005ccea2b2a39ba6b32e32fab5c97d4862cb4 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Mon, 29 Jan 2024 17:45:11 +0100
Subject: [PATCH 1/3] cleanup

---
 src/coq_elpi_utils.ml | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/src/coq_elpi_utils.ml b/src/coq_elpi_utils.ml
index a0a5d52ad..73501c5c0 100644
--- a/src/coq_elpi_utils.ml
+++ b/src/coq_elpi_utils.ml
@@ -71,7 +71,6 @@ module EC = EConstr
 
 let safe_destApp sigma t = match EC.kind sigma t with C.App (hd, args) -> (EC.kind sigma hd, args) | x -> (x, [||])
 let mkGHole = DAst.make Glob_term.(GHole GInternalHole)
-let mkGSort = DAst.make Glob_term.(GSort (UAnonymous { rigid = UState.univ_flexible_alg }))
 
 let mkApp ~depth t l =
   match l with
@@ -212,14 +211,6 @@ let rec list_map_acc f acc = function
       let acc, xs = list_map_acc f acc xs in
       (acc, x :: xs)
 
-let rec dest_globLam g =
-  match DAst.get g with
-  | Glob_term.GLambda (name, _, _, bo) ->
-      let names, bo = dest_globLam bo in
-      (name :: names, bo)
-  | _ -> ([], g)
-
-let is_unknown_constructor x = Names.GlobRef.ConstructRef x = Coqlib.lib_ref "elpi.unknown_constructor"
 let rec fix_detype x = match DAst.get x with Glob_term.GEvar _ -> mkGHole | _ -> Glob_ops.map_glob_constr fix_detype x
 
 let detype_qvar sigma q =

From b27693ca7dcef48cb0bfefd49e045dd5edcbb036 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Mon, 29 Jan 2024 17:45:26 +0100
Subject: [PATCH 2/3] test case for synterp bug

---
 tests/test_synterp.v | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

diff --git a/tests/test_synterp.v b/tests/test_synterp.v
index 403173581..bd957a3f5 100644
--- a/tests/test_synterp.v
+++ b/tests/test_synterp.v
@@ -156,4 +156,22 @@ Elpi Accumulate Db db1.
 Elpi Accumulate lp:{{ main _. }}.
 #[synterp] Elpi Accumulate lp:{{ main _. }}.
 
-Elpi Typecheck.
\ No newline at end of file
+Elpi Typecheck.
+
+(* ********************************************* *)
+
+Set Implicit Arguments.
+Elpi Command foo3.
+Elpi Accumulate lp:{{
+  main _ :-
+    D = (record "foo" {{ Type }} "mkfoo" (field [] "f" {{ Type }} _\end-record)),
+    coq.typecheck-indt-decl D ok,
+    coq.env.add-indt D I.
+}}.
+#[synterp] Elpi Accumulate lp:{{
+  main _ :- coq.env.begin-module "x" none, coq.env.end-module _.
+}}.
+Elpi foo3.
+
+
+

From 9e888e70d5cd67b07a34347907465ae8a48d67e7 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Mon, 29 Jan 2024 17:50:55 +0100
Subject: [PATCH 3/3] tentative fix

---
 src/coq_elpi_vernacular.ml | 5 +----
 tests/test_synterp.v       | 2 +-
 2 files changed, 2 insertions(+), 5 deletions(-)

diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml
index 3e23c7711..dc41a2119 100644
--- a/src/coq_elpi_vernacular.ml
+++ b/src/coq_elpi_vernacular.ml
@@ -567,10 +567,7 @@ module Interp = struct
         match syndata with
         | None -> [], fun ~target:_ ~depth -> Stdlib.Result.Ok ET.mkDiscard
         | Some (relocate_term,log) -> log, relocate_term in
-      let initial_synterp_state =
-        match synterplog with
-        | [] -> Vernacstate.Synterp.freeze ()
-        | x :: _ -> Coq_elpi_builtins_synterp.SynterpAction.synterp_state_after x in
+      let initial_synterp_state = Vernacstate.Synterp.freeze () in
       let query ~depth state =
         let state, args, gls = EU.map_acc
           (Coq_elpi_arg_HOAS.in_elpi_cmd ~depth ~raw:raw_args Coq_elpi_HOAS.(mk_coq_context ~options:(default_options ()) state))
diff --git a/tests/test_synterp.v b/tests/test_synterp.v
index bd957a3f5..3e16290ae 100644
--- a/tests/test_synterp.v
+++ b/tests/test_synterp.v
@@ -166,7 +166,7 @@ Elpi Accumulate lp:{{
   main _ :-
     D = (record "foo" {{ Type }} "mkfoo" (field [] "f" {{ Type }} _\end-record)),
     coq.typecheck-indt-decl D ok,
-    coq.env.add-indt D I.
+    coq.env.add-indt D I, coq.env.begin-module "x" none, coq.env.end-module _.
 }}.
 #[synterp] Elpi Accumulate lp:{{
   main _ :- coq.env.begin-module "x" none, coq.env.end-module _.