test case for synterp bug

LPCIC · Jan 31, 2024 · 4aa4a60 · 4aa4a60
1 parent cbe5233
commit 4aa4a60
Showing 1 changed file with 19 additions and 1 deletion.
diff --git 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.
+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.
+
+
+