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 ++++++++++++++
 src/tac2quote.ml  |  5 +++++
 src/tac2quote.mli |  3 +++
 3 files changed, 22 insertions(+)

(limited to 'src')

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
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index dbd2fd0529..f87e370032 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -233,6 +233,11 @@ let of_exact_hyp ?loc id =
   let refine = CTacRef (AbsKn (TacConstant (control_core "refine"))) in
   CTacApp (loc, refine, [thunk (of_hyp ~loc id)])
 
+let of_exact_var ?loc id =
+  let loc = Option.default dummy_loc loc in
+  let refine = CTacRef (AbsKn (TacConstant (control_core "refine"))) in
+  CTacApp (loc, refine, [thunk (of_variable id)])
+
 let of_dispatch tacs =
   let loc = Option.default dummy_loc (fst tacs) in
   let default = function
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index 7f3d9dce6e..b2687f01a3 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -58,6 +58,9 @@ val of_hyp : ?loc:Loc.t -> Id.t located -> raw_tacexpr
 val of_exact_hyp : ?loc:Loc.t -> Id.t located -> raw_tacexpr
 (** id ↦ 'Control.refine (fun () => Control.hyp @id') *)
 
+val of_exact_var : ?loc:Loc.t -> Id.t located -> raw_tacexpr
+(** id ↦ 'Control.refine (fun () => Control.hyp @id') *)
+
 val of_dispatch : dispatch -> raw_tacexpr
 
 val of_strategy_flag : strategy_flag -> raw_tacexpr
-- 
cgit v1.2.3