Don't reuse Coq AST for binding quotations.

This allows antiquotations in binding lists.

5 files changed, 35 insertions, 14 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index a09e99aa6b..71fb59acf8 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -19,7 +19,7 @@ open Ltac_plugin
 
 let err () = raise Stream.Failure
 
-(* idem for (x:=t) and (1:=t) *)
+(* lookahead for (x:=t), (?x:=t) and (1:=t) *)
 let test_lpar_idnum_coloneq =
   Gram.Entry.of_parser "test_lpar_idnum_coloneq"
     (fun strm ->
@@ -30,6 +30,13 @@ let test_lpar_idnum_coloneq =
                   (match stream_nth 2 strm with
                     | KEYWORD ":=" -> ()
                     | _ -> err ())
+              | LEFTQMARK ->
+                (match stream_nth 2 strm with
+                  | IDENT _ ->
+                      (match stream_nth 3 strm with
+                        | KEYWORD ":=" -> ()
+                        | _ -> err ())
+                  | _ -> err ())
               | _ -> err ())
         | _ -> err ())
 
@@ -282,30 +289,32 @@ GEXTEND Gram
   GLOBAL: q_ident q_bindings q_intropatterns;
   ident_or_anti:
     [ [ id = Prim.ident -> QExpr id
-      | "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id)
+      | LEFTQMARK; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id)
     ] ]
   ;
   q_ident:
     [ [ id = ident_or_anti -> Tac2quote.of_anti ~loc:!@loc Tac2quote.of_ident id ] ]
   ;
   simple_binding:
-    [ [ "("; id = Prim.ident; ":="; c = Constr.lconstr; ")" ->
-        Loc.tag ~loc:!@loc (NamedHyp id, Tac2quote.of_constr ~loc:!@loc c)
+    [ [ "("; LEFTQMARK; id = Prim.ident; ":="; c = Constr.lconstr; ")" ->
+        Loc.tag ~loc:!@loc (QAnti (Loc.tag ~loc:!@loc id), Tac2quote.of_constr ~loc:!@loc c)
       | "("; n = Prim.natural; ":="; c = Constr.lconstr; ")" ->
-        Loc.tag ~loc:!@loc (AnonHyp n, Tac2quote.of_constr ~loc:!@loc c)
+        Loc.tag ~loc:!@loc (QExpr (AnonHyp n), Tac2quote.of_constr ~loc:!@loc c)
+      | "("; id = Prim.ident; ":="; c = Constr.lconstr; ")" ->
+        Loc.tag ~loc:!@loc (QExpr (NamedHyp id), Tac2quote.of_constr ~loc:!@loc c)
     ] ]
   ;
   bindings:
     [ [ test_lpar_idnum_coloneq; bl = LIST1 simple_binding ->
-        Tac2quote.of_bindings ~loc:!@loc (ExplicitBindings bl)
+        QExplicitBindings bl
       | bl = LIST1 Constr.constr ->
         let bl = List.map (fun c -> Tac2quote.of_constr ~loc:!@loc c) bl in
-        Tac2quote.of_bindings ~loc:!@loc (Misctypes.ImplicitBindings bl)
+        QImplicitBindings bl
     ] ]
   ;
   q_bindings:
-    [ [ "with"; bl = bindings -> bl
-      | -> Tac2quote.of_bindings ~loc:!@loc Misctypes.NoBindings
+    [ [ "with"; bl = bindings -> Tac2quote.of_bindings ~loc:!@loc bl
+      | -> Tac2quote.of_bindings ~loc:!@loc QNoBindings
     ] ]
   ;
   intropatterns:
diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
index 794281cc75..b68efe73ac 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -9,6 +9,7 @@
 open Util
 open Loc
 open Names
+open Tac2expr
 
 (** Quoted variants of Ltac syntactic categories. Contrarily to the former, they
     sometimes allow anti-quotations. Used for notation scopes. *)
@@ -17,6 +18,11 @@ type 'a or_anti =
 | QExpr of 'a
 | QAnti of Id.t located
 
+type bindings =
+| QImplicitBindings of raw_tacexpr list
+| QExplicitBindings of (Misctypes.quantified_hypothesis or_anti * raw_tacexpr) Loc.located list
+| QNoBindings
+
 type intro_pattern =
 | QIntroForthcoming of bool
 | QIntroNaming of intro_pattern_naming
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index 96a3a5d9b8..488bcb5201 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -69,12 +69,12 @@ let of_qhyp ?loc = function
 | NamedHyp id -> constructor Core.c_named_hyp [of_ident ?loc id]
 
 let of_bindings ?loc = function
-| NoBindings ->
+| QNoBindings ->
   std_constructor ?loc "NoBindings" []
-| ImplicitBindings tl ->
+| QImplicitBindings tl ->
   std_constructor ?loc "ImplicitBindings" [of_list ?loc tl]
-| ExplicitBindings tl ->
-  let tl = List.map (fun (loc, (qhyp, e)) -> of_pair ?loc (of_qhyp ?loc qhyp, e)) tl in
+| QExplicitBindings tl ->
+  let tl = List.map (fun (loc, (qhyp, e)) -> of_pair ?loc (of_anti ?loc of_qhyp qhyp, e)) tl in
   std_constructor ?loc "ExplicitBindings" [of_list ?loc tl]
 
 let rec of_intro_pattern ?loc = function
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index 32973ff5ba..c9ee270d38 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -32,7 +32,7 @@ val of_constr : ?loc:Loc.t -> Constrexpr.constr_expr -> raw_tacexpr
 
 val of_list : ?loc:Loc.t -> raw_tacexpr list -> raw_tacexpr
 
-val of_bindings : ?loc:Loc.t -> raw_tacexpr bindings -> raw_tacexpr
+val of_bindings : ?loc:Loc.t -> bindings -> raw_tacexpr
 
 val of_intro_pattern : ?loc:Loc.t -> intro_pattern -> raw_tacexpr
 
diff --git a/tests/example2.v b/tests/example2.v
index 5efbf90b34..ffdb723ffb 100644
--- a/tests/example2.v
+++ b/tests/example2.v
@@ -13,3 +13,9 @@ Proof.
 split with 0.
 split.
 Qed.
+
+Goal exists n, n = 0.
+Proof.
+let myvar := Std.NamedHyp @x in split with (?myvar := 0).
+split.
+Qed.