Implementing Ltac2 antiquotations in constr syntax.

1 files changed, 14 insertions, 0 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index ae7e255896..672db12f1d 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -64,6 +64,16 @@ let test_ampersand_ident =
               | _ -> err ())
         | _ -> err ())
 
+let test_dollar_ident =
+  Gram.Entry.of_parser "test_dollar_ident"
+    (fun strm ->
+      match stream_nth 0 strm with
+        | IDENT "$" | KEYWORD "$" ->
+            (match stream_nth 1 strm with
+              | IDENT _ -> ()
+              | _ -> err ())
+        | _ -> err ())
+
 let tac2expr = Tac2entries.Pltac.tac2expr
 let tac2type = Gram.entry_create "tactic:tac2type"
 let tac2def_val = Gram.entry_create "tactic:tac2def_val"
@@ -649,6 +659,10 @@ GEXTEND Gram
         let tac = Tac2quote.of_exact_hyp ~loc:!@loc (Loc.tag ~loc:!@loc id) in
         let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in
         CAst.make ~loc:!@loc (CHole (None, IntroAnonymous, Some arg))
+      | test_dollar_ident; "$"; id = Prim.ident ->
+        let tac = Tac2quote.of_exact_var ~loc:!@loc (Loc.tag ~loc:!@loc id) in
+        let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in
+        CAst.make ~loc:!@loc (CHole (None, IntroAnonymous, Some arg))
     ] ]
   ;
 END