diff options
| author | herbelin | 2001-06-25 13:37:10 +0000 |
|---|---|---|
| committer | herbelin | 2001-06-25 13:37:10 +0000 |
| commit | 8ed67d4a2dabe40186c8ad0550fb3fbd2d9b8787 (patch) | |
| tree | 08a302bdd28b98df9da11751b831229ffc21cc04 /parsing/g_tactic.ml4 | |
| parent | 77259e0b563a10d57b55ac38400ca1843fb938f3 (diff) | |
Les réduction dans les hypothèses s'appliquent maintenant au corps de la définition en cas de LetIn (l'horrible syntaxe 'Unfold toto in (Type of hyp)' permet de forcer la réduction dans le type
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1806 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_tactic.ml4')
| -rw-r--r-- | parsing/g_tactic.ml4 | 25 |
1 files changed, 16 insertions, 9 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) >> |