diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-02 21:58:58 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-02 21:58:58 +0000 |
| commit | 836c28c4027b9626be4ca5371cc6559517fd7d1e (patch) | |
| tree | de5a5f2457652fd0af66fecf008b8bd0482e0ed2 /parsing | |
| parent | f07684f5d77802f8ed286fdbf234bd542b689e45 (diff) | |
Extension syntaxique de rewrite in: au lieu de pouvoir faire
juste rewrite in <id>, on a maintenant rewrite in <clause>.
Ainsi rewrite H in H1,H2 |- * === rewrite H in H1; rewrite H in H2; rewrite H
Pour l'instant rewrite H in * |- signifie: faire une fois
"try rewrite H in Hi" sur toutes les hypotheses Hi du contexte sauf H
En particulier, n'echoue pour l'instant pas s'il n'y a rien a
reecrire nulle part.
NB: rewrite H in * === rewrite H in * |- * === rewrite H in * |- ; rewrite H
ATTENTION: la syntaxe de rewrite ayant changé, j'adapte interface en conséquence.
Est-ce la bonne facon de faire ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8780 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 7 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 5 |
2 files changed, 12 insertions, 0 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 5c847f5a4..d87336b81 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -261,6 +261,11 @@ GEXTEND Gram [ [ "in"; idl = LIST1 id_or_meta -> idl | -> [] ] ] ; + orient: + [ [ "->" -> true + | "<-" -> false + | -> true ]] + ; fixdecl: [ [ "("; id = ident; bl=LIST0 Constr.binder; ann=fixannot; ":"; ty=lconstr; ")" -> (loc,id,bl,ann,ty) ] ] @@ -411,6 +416,8 @@ GEXTEND Gram | IDENT "transitivity"; c = constr -> TacTransitivity c (* Equality and inversion *) + | IDENT "rewrite"; b = orient; c = constr_with_bindings ; cl = clause -> + TacRewrite (b,c,cl) | IDENT "dependent"; k = [ IDENT "simple"; IDENT "inversion" -> SimpleInversion | IDENT "inversion" -> FullInversion diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 76054c599..f1388ab69 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -418,6 +418,8 @@ let pr_clause_pattern pr_id = function ++ spc () ++ pr_id id) l ++ pr_opt (fun nl -> prlist_with_sep spc int nl ++ str " Goal") glopt +let pr_orient b = if b then mt () else str " <-" + let pr_induction_arg prc = function | ElimOnConstr c -> prc c | ElimOnIdent (loc,id) -> pr_with_comments loc (pr_id id) @@ -787,6 +789,9 @@ and pr_atom1 env = function | TacTransitivity c -> str "transitivity" ++ pr_constrarg env c (* Equality and inversion *) + | TacRewrite (b,c,cl) -> + hov 1 (str "rewrite" ++ pr_orient b ++ spc() ++ pr_with_bindings env c ++ + pr_clauses pr_ident cl) | TacInversion (DepInversion (k,c,ids),hyp) -> hov 1 (str "dependent " ++ pr_induction_kind k ++ spc () ++ pr_quantified_hypothesis hyp ++ |