Implementing Ltac2 antiquotations in constr syntax.

4 files changed, 29 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
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
diff --git a/tests/quot.v b/tests/quot.v
index c9aa1f9d14..4fa9c4fa4e 100644
--- a/tests/quot.v
+++ b/tests/quot.v
@@ -7,3 +7,10 @@ Ltac2 ref1 () := reference:(nat).
 Ltac2 ref2 () := reference:(Datatypes.nat).
 Fail Ltac2 ref () := reference:(i_certainly_dont_exist).
 Fail Ltac2 ref () := reference:(And.Me.neither).
+
+Goal True.
+Proof.
+let x := constr:(I) in
+let y := constr:((fun z => z) $x) in
+Control.refine (fun _ => y).
+Qed.