- Temptative change to notations like "as [|n H]_eqn" or "as [|n H]_eqn:H",

  and, with a now generic intropattern "[]", also "as []_eqn", "as []_eqn:H"
  for "destruct" with equality keeping.
- Fixed an accuracy loss in error location.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11732 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 3 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 1f4aa8b24..a531770a4 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -257,6 +257,11 @@ GEXTEND Gram
       | "?" -> loc, IntroAnonymous
       | id = ident -> loc, IntroIdentifier id ] ]
   ;
+  intropattern_modifier:
+    [ [ IDENT "_eqn"; 
+        id = [ ":"; id = naming_intropattern -> id | -> loc, IntroAnonymous ]
+        -> id ] ]
+  ;
   simple_intropattern:
     [ [ pat = disjunctive_intropattern -> pat
       | pat = naming_intropattern -> pat
@@ -415,13 +420,12 @@ GEXTEND Gram
       | -> None ] ]
   ;
   with_inversion_names:
-    [ [ "as"; ipat = disjunctive_intropattern -> Some ipat
+    [ [ "as"; ipat = simple_intropattern -> Some ipat
       | -> None ] ]
   ;
   with_induction_names:
-    [ [ "as"; eq = OPT naming_intropattern; ipat = disjunctive_intropattern
+    [ [ "as"; ipat = simple_intropattern; eq = OPT intropattern_modifier
         -> (eq,Some ipat)
-      | "as"; eq = naming_intropattern -> (Some eq,None)
       | -> (None,None) ] ]
   ;
   as_name: