From 73ecd7e2f0136234f73f405a569858f2b0ecee9b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 1 Aug 2017 16:56:27 +0200
Subject: Fix parsing of fresh ident antiquotations.

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

(limited to 'src')

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index b058680645..a09e99aa6b 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -335,8 +335,9 @@ GEXTEND Gram
       | "[="; tc = intropatterns; "]" -> QIntroInjection tc ] ]
   ;
   naming_intropattern:
-    [ [ LEFTQMARK; prefix = ident_or_anti -> QIntroFresh prefix
-      | LEFTQMARK -> QIntroAnonymous
+    [ [ LEFTQMARK; id = Prim.ident -> QIntroFresh (QExpr id)
+      | "?$"; id = Prim.ident -> QIntroFresh (QAnti (Loc.tag ~loc:!@loc id))
+      | "?" -> QIntroAnonymous
       | id = ident_or_anti -> QIntroIdentifier id ] ]
   ;
   nonsimple_intropattern:
-- 
cgit v1.2.3