From c3d83f8437022986593df45c3c3920c8356d9f84 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 25 Aug 2017 14:51:20 +0200
Subject: Lookahead to cheat the constr parser in order to parse "& IDENT".

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

(limited to 'src')

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 7406a45207..3d873c7369 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -54,6 +54,16 @@ let test_lpar_id_rpar =
 	      | _ -> err ())
 	| _ -> err ())
 
+let test_ampersand_ident =
+  Gram.Entry.of_parser "test_ampersand_ident"
+    (fun strm ->
+      match stream_nth 0 strm with
+        | 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"
@@ -617,8 +627,8 @@ GEXTEND Gram
     [ [ 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))
-      | "&"; id = [ id = Prim.ident -> Loc.tag ~loc:!@loc id ] ->
-        let tac = Tac2quote.of_exact_hyp ~loc:!@loc id in
+      | test_ampersand_ident; "&"; id = Prim.ident ->
+        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))
     ] ]
-- 
cgit v1.2.3