test case for synterp bug

Author: gares

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.
+}}.
+#[synterp] Elpi Accumulate lp:{{
+  main _ :- coq.env.begin-module "x" none, coq.env.end-module _.
+}}.
+Elpi foo3.
+
+
+