From be38f04cd06d3c044b66b9ccee34dd1a775eb306 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 27 Nov 2024 23:17:40 +0100
Subject: [PATCH] syntax `( term )

---
 README.md                   | 1 +
 src/coq_elpi_arg_syntax.mlg | 1 +
 tests/test_arg_HOAS.v       | 8 ++++++++
 3 files changed, 10 insertions(+)

diff --git a/README.md b/README.md
index 3d53876ed..d25eaae6c 100644
--- a/README.md
+++ b/README.md
@@ -419,6 +419,7 @@ tactic receives `open-trm N F` where `N` is the number of free variables in `U`
 and `F` is `fun x1 => ... fun xN => U`.
 Finally, `ltac_term:(T)` and `(T)` are *not* synonyms: but the former must be used
 when defining tactic notations, the latter when invoking elpi tactics directly.
+``` `(T)``` can be used to pass an open term to `elpi tactic ...`.
 
 ##### Attributes
 
diff --git a/src/coq_elpi_arg_syntax.mlg b/src/coq_elpi_arg_syntax.mlg
index b43894bdd..1467ddff2 100644
--- a/src/coq_elpi_arg_syntax.mlg
+++ b/src/coq_elpi_arg_syntax.mlg
@@ -327,6 +327,7 @@ TYPED AS elpi_ftactic_arg
 | [ integer(n) ] -> { EA.Tac.Int n }
 | [ string(s) ] -> { EA.Tac.String s }
 | [ "(" lconstr(t) ")" ] -> { EA.Tac.Term t }
+| [ "`(" lconstr(t) ")" ] -> { EA.Tac.OpenTerm t }
 | [ "ltac_string" ":" "(" ident(t) ")" ] -> { EA.Tac.LTac(EA.Tac.String, (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) }
 | [ "ltac_string_list" ":" "(" ident(t) ")" ] -> { EA.Tac.LTac(EA.Tac.List EA.Tac.String, (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) }
 | [ "ltac_int" ":" "(" ident(t) ")" ] -> { EA.Tac.LTac(EA.Tac.Int, (CAst.make ~loc @@ Constrexpr.CRef (Libnames.qualid_of_string ~loc @@ Names.Id.to_string t,None))) }
diff --git a/tests/test_arg_HOAS.v b/tests/test_arg_HOAS.v
index 5a32492c6..8594975fe 100644
--- a/tests/test_arg_HOAS.v
+++ b/tests/test_arg_HOAS.v
@@ -385,3 +385,11 @@ Elpi bug_394
   Definition D `{L} : Prop := True
   Definition D `{L} (n:nat) : Prop := True
   .
+
+Elpi Tactic open.
+Elpi Accumulate lp:{{
+solve (goal _ _ _ _ [open-trm N X]) _ :- coq.say N X.
+}}.
+Goal True.
+elpi open `(x + y).
+Abort.