diff options
| author | herbelin | 2000-12-20 17:03:15 +0000 |
|---|---|---|
| committer | herbelin | 2000-12-20 17:03:15 +0000 |
| commit | dd8b4d6384b0db16e54877ea7d2487deff48e934 (patch) | |
| tree | cca8b179698cb6082d81a539a9bf44a3253aeab4 | |
| 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
| -rw-r--r-- | parsing/g_tactic.ml4 | 16 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 3 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 1 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 1 |
4 files changed, 14 insertions, 7 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index cb85e676dc..99e7e136e5 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) >> diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 9f10f19412..2eab116658 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -227,6 +227,9 @@ GEXTEND Gram field: [ [ id = identarg; oc = of_type_with_opt_coercion; c = constrarg -> <:ast< (VERNACARGLIST ($STR $oc) $id $c) >> + | id = identarg; ":="; b = constrarg; + oc = of_type_with_opt_coercion; c = constrarg -> + <:ast< (VERNACARGLIST ($STR $oc) $id $c $b) >> (* | id = identarg; ":>"; c = constrarg -> <:ast< (VERNACARGLIST "COERCION" $id $c) >> *)] ] ; diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index fbbec9b34f..b109218177 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -282,6 +282,7 @@ module Tactic = let numarg_binding_list = gec_list "numarg_binding_list" let lconstrarg_binding_list = gec_list "lconstrarg_binding_list" let constrarg_list = gec_list "constrarg_list" + let ident_or_constrarg = gec "ident_or_constrarg" let identarg = gec "identarg" let qualidarg = gec "qualidarg" let qualidconstarg = gec "qualidconstarg" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 960a59be7f..c4f61aa75d 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -111,6 +111,7 @@ module Tactic : val constrarg_binding_list : Coqast.t list Gram.Entry.e val constrarg_list : Coqast.t list Gram.Entry.e val fixdecl : Coqast.t list Gram.Entry.e + val ident_or_constrarg : Coqast.t Gram.Entry.e val identarg : Coqast.t Gram.Entry.e val qualidarg : Coqast.t Gram.Entry.e val qualidconstarg : Coqast.t Gram.Entry.e |