aboutsummaryrefslogtreecommitdiff
path: root/dev/doc
diff options
context:
space:
mode:
Diffstat (limited to 'dev/doc')
-rw-r--r--dev/doc/changes.txt4
1 files changed, 4 insertions, 0 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 7b2b1ca28f..784283358a 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -2,6 +2,10 @@
= CHANGES BETWEEN COQ V8.3 AND COQ V8.4 =
=========================================
+** Removal of Tacinterp.constr_of_id **
+
+Use instead either global_reference or construct_reference in constrintern.ml.
+
** Optimizing calls to Evd functions **
Evars are split into defined evars and undefined evars; for