syntax `( term )

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
 

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

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.