From 9ec08ac299faf6acdfd6061fd21a00e3446aec79 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 24 Sep 2014 15:03:34 +0200
Subject: Using an or_var rather than the hack with loc for coding a pure ident
 as a disjunctive intropattern.

---
 parsing/g_tactic.ml4 | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 5ffabbcf55..4b9d223ad7 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -476,12 +476,8 @@ GEXTEND Gram
       | -> None ] ]
   ;
   or_and_intropattern_loc:
-    [ [ ipat = or_and_intropattern -> !@loc, ipat
-      | id = ident ->
-          !@loc,
-          (* coding, see tacinterp.ml: *)
-          [[Loc.ghost, IntroNaming (IntroIdentifier id)]]
-      ] ]
+    [ [ ipat = or_and_intropattern -> ArgArg (!@loc,ipat)
+      | locid = identref -> ArgVar locid ] ]
   ;
   as_or_and_ipat:
     [ [ "as"; ipat = or_and_intropattern_loc -> Some ipat
-- 
cgit v1.2.3