Properly implementing the notation to easily access hypotheses.

3 files changed, 37 insertions, 3 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index f558f9b9cc..bb98ea3e5d 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -136,6 +136,7 @@ GEXTEND Gram
       | id = Prim.qualid ->
         if Tac2env.is_constructor (snd id) then CTacCst (!@loc, RelId id) else CTacRef (RelId id)
       | "@"; id = Prim.ident -> Tac2quote.of_ident ~loc:!@loc id
+      | "&"; id = Prim.ident -> Tac2quote.of_hyp ~loc:!@loc id
       | "'"; c = Constr.constr -> inj_open_constr !@loc c
       | IDENT "constr"; ":"; "("; c = Constr.lconstr; ")" -> Tac2quote.of_constr ~loc:!@loc c
       | IDENT "open_constr"; ":"; "("; c = Constr.lconstr; ")" -> inj_open_constr !@loc c
@@ -381,8 +382,13 @@ END
 GEXTEND Gram
   Pcoq.Constr.operconstr: LEVEL "0"
     [ [ IDENT "ltac2"; ":"; "("; tac = tac2expr; ")" ->
-          let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in
-          CAst.make ~loc:!@loc (CHole (None, IntroAnonymous, Some arg)) ] ]
+        let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in
+        CAst.make ~loc:!@loc (CHole (None, IntroAnonymous, Some arg))
+      | "&"; id = Prim.ident ->
+        let tac = Tac2quote.of_exact_hyp ~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 0e0a7b3fce..e30acc48ab 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -17,7 +17,13 @@ open Tac2core
 
 (** Syntactic quoting of expressions. *)
 
-let std_core n = KerName.make2 Tac2env.std_prefix (Label.of_id (Id.of_string n))
+let control_prefix =
+  MPfile (DirPath.make (List.map Id.of_string ["Control"; "Ltac2"]))
+
+let kername prefix n = KerName.make2 prefix (Label.of_id (Id.of_string n))
+let std_core n = kername Tac2env.std_prefix n
+let coq_core n = kername Tac2env.coq_prefix n
+let control_core n = kername control_prefix n
 
 let dummy_loc = Loc.make_loc (-1, -1)
 
@@ -114,3 +120,19 @@ and of_or_and_intro_pattern ?loc = function
 
 and of_intro_patterns ?loc l =
   of_list ?loc (List.map (of_intro_pattern ?loc) l)
+
+let of_hyp ?loc id =
+  let loc = Option.default dummy_loc loc in
+  let hyp = CTacRef (AbsKn (control_core "hyp")) in
+  CTacApp (loc, hyp, [of_ident ~loc id])
+
+let thunk e =
+  let t_unit = coq_core "unit" in
+  let loc = Tac2intern.loc_of_tacexpr e in
+  let var = [CPatVar (Some loc, Anonymous), Some (CTypRef (loc, AbsKn (Other t_unit), []))] in
+  CTacFun (loc, var, e)
+
+let of_exact_hyp ?loc id =
+  let loc = Option.default dummy_loc loc in
+  let refine = CTacRef (AbsKn (control_core "refine")) in
+  CTacApp (loc, refine, [thunk (of_hyp ~loc id)])
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index a311430a66..4cbe854f75 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -39,3 +39,9 @@ val of_bindings : ?loc:Loc.t -> bindings -> raw_tacexpr
 val of_intro_pattern : ?loc:Loc.t -> intro_pattern -> raw_tacexpr
 
 val of_intro_patterns : ?loc:Loc.t -> intro_pattern list -> raw_tacexpr
+
+val of_hyp : ?loc:Loc.t -> Id.t -> raw_tacexpr
+(** id ↦ 'Control.hyp @id' *)
+
+val of_exact_hyp : ?loc:Loc.t -> Id.t -> raw_tacexpr
+(** id ↦ 'Control.refine (fun () => Control.hyp @id') *)