diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-04-28 09:34:32 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-04-28 09:34:32 +0000 |
| commit | b61d0df2899f5de9c20ee4a2c4b79deb0714b162 (patch) | |
| tree | 6c548a7046878591025baae80b4ead8d5b349c2a /dev/doc/changes.txt | |
| parent | 2ed87ba29db49e043062e125f3783a553d550fc4 (diff) | |
Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.
Fusion des syntaxes de "apply" et "eapply". Ajout de "eapply in",
"erewrite" et "erewrite in". Correction au passage des bugs #1461 et
#1522).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9802 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/doc/changes.txt')
| -rw-r--r-- | dev/doc/changes.txt | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index ad5704db8..ad7eaaf5e 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -8,7 +8,8 @@ A few differences in Coq ML interfaces between Coq V8.0 and V8.1 ** Functions Eauto: e_resolve_constr, vernac_e_resolve_constr -> simplest_eapply - +Tactics: apply_with_bindings -> apply_with_bindings_wo_evars +Eauto.simplest_apply -> Hiddentac.h_simplest_apply ========================================= = CHANGES BETWEEN COQ V8.0 AND COQ V8.1 = |