aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/doc/changes.txt3
1 files changed, 2 insertions, 1 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index ad5704db8e..ad7eaaf5e7 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 =