diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 25 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 5 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 5 |
3 files changed, 24 insertions, 11 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 70aaba18d1..c374f59557 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -54,6 +54,9 @@ GEXTEND Gram [ [ id = Constr.ident -> id | "?"; n = Prim.number -> <:ast< (COMMAND (META $n)) >> ] ] ; + idmetahyp: + [ [ id = idmeta_arg -> <:ast< (INHYP $id) >> ] ] + ; qualidarg: [ [ l = Constr.qualid -> <:ast< (QUALIDARG ($LIST l)) >> | "?"; n = Prim.number -> <:ast< (QUALIDMETA $n) >> ] ] @@ -94,8 +97,8 @@ GEXTEND Gram ne_identarg_list: [ [ l = LIST1 identarg -> l ] ] ; - ne_idmeta_arg_list: - [ [ l = LIST1 idmeta_arg -> l ] ] + ne_idmetahyp_list: + [ [ l = LIST1 idmetahyp -> l ] ] ; ne_qualidarg_list: [ [ l = LIST1 qualidarg -> l ] ] @@ -211,8 +214,15 @@ GEXTEND Gram | IDENT "Pattern"; pl = ne_pattern_list -> <:ast< (Pattern ($LIST $pl)) >> ] ] ; + hypident: + [ [ id = identarg -> <:ast< (INHYP $id) >> + | "("; "Type"; "of"; id = identarg; ")" -> <:ast< (INHYPTYPE $id) >> ] ] + ; + ne_hyp_list: + [ [ l = LIST1 hypident -> l ] ] + ; clausearg: - [ [ "in"; idl = ne_identarg_list -> <:ast< (CLAUSE ($LIST idl)) >> + [ [ "in"; idl = ne_hyp_list -> <:ast< (CLAUSE ($LIST idl)) >> | -> <:ast< (CLAUSE) >> ] ] ; fixdecl: @@ -225,9 +235,6 @@ GEXTEND Gram <:ast< (COFIXEXP $id $c) >> :: fd | -> [] ] ] ; - END - -GEXTEND Gram simple_tactic: [ [ IDENT "Fix"; n = pure_numarg -> <:ast< (Fix $n) >> | IDENT "Fix"; id = identarg; n = pure_numarg -> <:ast< (Fix $id $n) >> @@ -300,8 +307,8 @@ GEXTEND Gram <:ast< (DecomposeAnd $c) >> | IDENT "Decompose"; IDENT "Sum"; c = constrarg -> <:ast< (DecomposeOr $c) >> - | IDENT "Decompose"; "["; l = ne_identarg_list; "]"; c = constrarg -> - <:ast< (DecomposeThese (CLAUSE ($LIST $l)) $c) >> + | IDENT "Decompose"; "["; l = ne_qualidarg_list; "]"; c = constrarg -> + <:ast< (DecomposeThese $c ($LIST $l)) >> | IDENT "Cut"; c = constrarg -> <:ast< (Cut $c) >> | IDENT "Specialize"; n = pure_numarg; lcb = constrarg_binding_list -> <:ast< (Specialize $n ($LIST $lcb))>> @@ -314,7 +321,7 @@ GEXTEND Gram | IDENT "LetTac"; s = identarg; ":="; c = constrarg; p = clause_pattern-> <:ast< (LetTac $s $c $p) >> | IDENT "LApply"; c = constrarg -> <:ast< (CutAndApply $c) >> - | IDENT "Clear"; l = ne_idmeta_arg_list -> + | IDENT "Clear"; l = ne_idmetahyp_list -> <:ast< (Clear (CLAUSE ($LIST $l))) >> | IDENT "Move"; id1 = identarg; IDENT "after"; id2 = identarg -> <:ast< (MoveDep $id1 $id2) >> diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index ff103ae2ca..849d2639cc 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -292,7 +292,9 @@ module Tactic = let constrarg_list = gec_list "constrarg_list" let ident_or_constrarg = gec "ident_or_constrarg" let identarg = gec "identarg" + let hypident = gec "hypident" let idmeta_arg = gec "idmeta_arg" + let idmetahyp = gec "idmetahyp" let qualidarg = gec "qualidarg" let qualidconstarg = gec "qualidconstarg" let input_fun = gec "input_fun" @@ -307,7 +309,8 @@ module Tactic = let match_rule = gec "match_rule" let match_list = gec_list "match_list" let ne_identarg_list = gec_list "ne_identarg_list" - let ne_idmeta_arg_list = gec_list "ne_idmeta_arg_list" + let ne_hyp_list = gec_list "ne_hyp_list" + let ne_idmetahyp_list = gec_list "ne_idmetahyp_list" let ne_qualidarg_list = gec_list "ne_qualidarg_list" let ne_qualidconstarg_list = gec_list "ne_qualidconstarg_list" let ne_pattern_list = gec_list "ne_pattern_list" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 30773eaa6a..b9c77509e2 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -116,7 +116,9 @@ module Tactic : 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 hypident : Coqast.t Gram.Entry.e val idmeta_arg : Coqast.t Gram.Entry.e + val idmetahyp : Coqast.t Gram.Entry.e val qualidarg : Coqast.t Gram.Entry.e val qualidconstarg : Coqast.t Gram.Entry.e val input_fun : Coqast.t Gram.Entry.e @@ -132,7 +134,8 @@ module Tactic : val match_rule : Coqast.t Gram.Entry.e val match_list : Coqast.t list Gram.Entry.e val ne_identarg_list : Coqast.t list Gram.Entry.e - val ne_idmeta_arg_list : Coqast.t list Gram.Entry.e + val ne_hyp_list : Coqast.t list Gram.Entry.e + val ne_idmetahyp_list : Coqast.t list Gram.Entry.e val ne_qualidarg_list : Coqast.t list Gram.Entry.e val ne_qualidconstarg_list : Coqast.t list Gram.Entry.e val ne_intropattern : Coqast.t Gram.Entry.e |