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 /contrib/interface/ascent.mli | |
| 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 'contrib/interface/ascent.mli')
| -rw-r--r-- | contrib/interface/ascent.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli index fb71288a9..8f880a767 100644 --- a/contrib/interface/ascent.mli +++ b/contrib/interface/ascent.mli @@ -685,8 +685,8 @@ and ct_TACTIC_COM = | CT_rename of ct_ID * ct_ID | CT_repeat of ct_TACTIC_COM | CT_replace_with of ct_FORMULA * ct_FORMULA * ct_ID_OPT * ct_TACTIC_OPT - | CT_rewrite_lr of ct_FORMULA * ct_SPEC_LIST * ct_ID_OPT - | CT_rewrite_rl of ct_FORMULA * ct_SPEC_LIST * ct_ID_OPT + | CT_rewrite_lr of ct_FORMULA * ct_SPEC_LIST * ct_CLAUSE + | CT_rewrite_rl of ct_FORMULA * ct_SPEC_LIST * ct_CLAUSE | CT_right of ct_SPEC_LIST | CT_ring of ct_FORMULA_LIST | CT_simple_user_tac of ct_ID * ct_TACTIC_ARG_LIST |