From db03c10aaafd3c0128a5b7504f14d4b7aaca842e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 29 Aug 2017 01:16:21 +0200
Subject: Implementing Ltac2 antiquotations in constr syntax.

---
 src/g_ltac2.ml4 | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'src/g_ltac2.ml4')

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
-- 
cgit v1.2.3