tentative fix

LPCIC · Jan 31, 2024 · 013af6b · 013af6b
1 parent 4aa4a60
commit 013af6b
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 5 deletions.
diff --git 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
@@ -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 _.