diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-20 17:03:15 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-20 17:03:15 +0000 |
| commit | dd8b4d6384b0db16e54877ea7d2487deff48e934 (patch) | |
| tree | cca8b179698cb6082d81a539a9bf44a3253aeab4 /parsing/g_tactic.ml4 | |
| parent | ff8dd1511ee4af7e9fe797757091e32913ee4e4a (diff) | |
ajout ident_or_constrarg pour NewInduction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1167 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_tactic.ml4')
| -rw-r--r-- | parsing/g_tactic.ml4 | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index cb85e676d..99e7e136e 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -47,6 +47,13 @@ GEXTEND Gram castedconstrarg: [ [ c = Constr.constr -> <:ast< (CASTEDCOMMAND $c) >> ] ] ; + ident_or_constrarg: + [ [ c = Constr.constr -> + match c with + | Coqast.Nvar(_,s) -> <:ast<($VAR $s)>> + | Coqast.Node(_,"QUALID",[Coqast.Nvar(_,s)]) -> <:ast<($VAR $s)>> + | _ -> <:ast< (COMMAND $c) >> ] ] + ; ne_identarg_list: [ [ l = LIST1 identarg -> l ] ] ; @@ -301,12 +308,7 @@ GEXTEND Gram | "?"; n = Prim.number -> <:ast< (COMMAND (META $n)) >> | IDENT "Eval"; rtc = Tactic.red_tactic; "in"; c = Constr.constr -> <:ast< (COMMAND (EVAL $c (REDEXP $rtc))) >> - | "'"; c = constrarg -> - (match c with - | Coqast.Node(_,"COMMAND",[Coqast.Nvar(_,s)]) -> <:ast<($VAR $s)>> - | Coqast.Node(_,"COMMAND",[Coqast.Node(_,"QUALID", - [Coqast.Nvar(_,s)])]) -> <:ast<($VAR $s)>> - |_ -> c) ] ] + | "'"; c = ident_or_constrarg -> c ] ] ; simple_tactic: [ [ IDENT "Fix"; n = pure_numarg -> <:ast< (Fix $n) >> @@ -319,7 +321,7 @@ GEXTEND Gram <:ast< (Cofix $id ($LIST $fd)) >> | IDENT "Induction"; s = identarg -> <:ast< (Induction $s) >> | IDENT "Induction"; n = pure_numarg -> <:ast< (Induction $n) >> - | IDENT "NewInduction"; c = constrarg -> <:ast< (NewInduction $c) >> + | IDENT "NewInduction"; c=ident_or_constrarg -> <:ast<(NewInduction $c)>> | IDENT "NewInduction"; n = pure_numarg -> <:ast< (NewInduction $n) >> | IDENT "Double"; IDENT "Induction"; i = numarg; j = numarg -> <:ast< (DoubleInd $i $j) >> |