diff options
| author | herbelin | 2000-11-26 18:55:00 +0000 |
|---|---|---|
| committer | herbelin | 2000-11-26 18:55:00 +0000 |
| commit | eea969b42e6a7770f7e0c80cc3d2a12690216322 (patch) | |
| tree | 2da9a57e9b267a6d291ac87fee2ea07c4640c80e /parsing | |
| parent | 98133e7cbbe9e97ac31437e59bc4f534f02360ce (diff) | |
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
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 5 |
1 files changed, 3 insertions, 2 deletions
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)>> |