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 /proofs | |
| 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 'proofs')
| -rw-r--r-- | proofs/tacexpr.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index ea7c49f2b..89060f9cc 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -184,6 +184,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacTransitivity of 'constr (* Equality and inversion *) + | TacRewrite of bool * 'constr with_bindings * 'id gclause | TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis (* For ML extensions *) |