Merge pull request #583 from LPCIC/fix-synter-impargs

Fix synter impargs

Author: gares

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 =

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))

tests/test_synterp.v

@@ -156,4 +156,22 @@ Elpi Accumulate Db db1.
 Elpi Accumulate lp:{{ main _. }}.
 #[synterp] Elpi Accumulate lp:{{ main _. }}.
 
-Elpi Typecheck.
+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, 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 _.
+}}.
+Elpi foo3.
+
+
+