From eea969b42e6a7770f7e0c80cc3d2a12690216322 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 26 Nov 2000 18:55:00 +0000
Subject: Distinction claire entre Induction (nom interne : raw_induct) et le
 nouvel induction (now temporaire NewInduction)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@960 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_tactic.ml4 | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 39bdda79bd..66b016cfce 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -16,8 +16,7 @@ open Util
 GEXTEND Gram
 
   identarg:
-    [ [ id = IDENT -> <:ast< ($VAR $id) >> 
-      | id = METAIDENT -> <:ast< ($VAR $id) >> ] ]
+    [ [ id = Constr.ident -> id ] ]
   ;
   qualidarg:
     [ [ l = Constr.qualid -> <:ast< (QUALIDARG ($LIST l)) >> ] ]
@@ -311,6 +310,8 @@ GEXTEND Gram
           <:ast< (Cofix $id ($LIST $fd)) >>
       | IDENT "Induction"; s = identarg -> <:ast< (Induction $s) >>
       | IDENT "Induction"; n = numarg -> <:ast< (Induction $n) >>
+      | IDENT "NewInduction"; c = constrarg -> <:ast< (NewInduction $c) >>
+      | IDENT "NewInduction"; n = numarg -> <:ast< (NewInduction $n) >>
       | IDENT "Double"; IDENT "Induction"; i = numarg; j = numarg ->
           <:ast< (DoubleInd $i $j) >>
       | IDENT "Trivial" -> <:ast<(Trivial)>>
-- 
cgit v1.2.3