From b61d0df2899f5de9c20ee4a2c4b79deb0714b162 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 28 Apr 2007 09:34:32 +0000 Subject: 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). MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9802 85f007b7-540e-0410-9357-904b9bb8a0f7 --- dev/doc/changes.txt | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'dev/doc/changes.txt') 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 = -- cgit v1.2.3