La grammaire n'était plus LL1

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

1 files changed, 14 insertions, 5 deletions

diff --git a/tactics/Inv.v b/tactics/Inv.v
index 12633311df..39a434b010 100644
--- a/tactics/Inv.v
+++ b/tactics/Inv.v
@@ -34,20 +34,29 @@ Syntax tactic level 0:
 
 
 Grammar tactic simple_tactic: ast :=
-  inversion    [ inversion_com($ic) ident_or_numarg($id) ] -> [(Inv $ic $id)]
+  inversion    [ inversion_com($ic) identarg($id) ] -> [(Inv $ic $id)]
+| inversion_num [ inversion_com($ic) pure_numarg($n) ] -> [(Inv $ic $n)]
 | inversion_in [ inversion_com($ic) identarg($id) "in" ne_identarg_list($l) ]
       -> [(InvIn $ic $id ($LIST $l))]
-| dep_inv   [ "Dependent" inversion_com($ic) ident_or_numarg($id) ]
-     -> [(DInv $ic $id)]
+| dep_inv   [ "Dependent" inversion_com($ic) identarg($id)] -> [(DInv $ic $id)]
+| dep_inv_num  [ "Dependent" inversion_com($ic) pure_numarg($n) ] -> [(DInv $ic $n)]
 | dep_inv_with
-   [ "Dependent" inversion_com($ic) ident_or_numarg($id) "with" constrarg($c) ]
+   [ "Dependent" inversion_com($ic) identarg($id) "with" constrarg($c) ]
      -> [(DInvWith $ic $id $c) ]
+| dep_inv_num_with
+   [ "Dependent" inversion_com($ic) pure_numarg($n) "with" constrarg($c) ]
+     -> [(DInvWith $ic $n $c) ]
 
-| inv_using [ inversion_com($ic) ident_or_numarg($id) "using" constrarg($c) ]
+| inv_using [ inversion_com($ic) identarg($id) "using" constrarg($c) ]
      -> case [$ic] of
           Inversion -> [(UseInversionLemma $id $c)]
         esac
 
+| inv_num_using [ inversion_com($ic) pure_numarg($n) "using" constrarg($c) ]
+     -> case [$ic] of
+          Inversion -> [(UseInversionLemma $n $c)]
+        esac
+
 | inv_using_in
    [ inversion_com($ic) identarg($id) "using" constrarg($c)
      "in" ne_identarg_list($l) ]