diff options
| author | letouzey | 2006-05-02 21:58:58 +0000 |
|---|---|---|
| committer | letouzey | 2006-05-02 21:58:58 +0000 |
| commit | 836c28c4027b9626be4ca5371cc6559517fd7d1e (patch) | |
| tree | de5a5f2457652fd0af66fecf008b8bd0482e0ed2 /scripts | |
| 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 'scripts')
0 files changed, 0 insertions, 0 deletions