aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/doc/changes.txt
diff options
context:
space:
mode:
Diffstat (limited to 'dev/doc/changes.txt')
-rw-r--r--dev/doc/changes.txt3
1 files changed, 3 insertions, 0 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 2164830a7..d4e42142b 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -75,6 +75,9 @@
check_evars_are_solved explicitly to check that evars are solved.
See also the corresponding commit log.
+- Tactics API: new_induct -> induction; new_destruct -> destruct;
+ letin_pat_tac do not accept a type anymore
+
=========================================
= CHANGES BETWEEN COQ V8.3 AND COQ V8.4 =
=========================================