1 files changed, 39 insertions, 0 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 069f7d42..322530e6 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -1,4 +1,43 @@
 =========================================
+= CHANGES BETWEEN COQ V8.3 AND COQ V8.4 =
+=========================================
+
+** Functions in unification.ml have now the evar_map coming just after the env
+
+** 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
+efficiency, when an evar is known to be undefined, it is preferable to
+use specific functions about undefined evars since these ones are
+generally fewer than the defined ones.
+
+** Type changes in TACTIC EXTEND rules **
+
+Arguments bound with tactic(_) in TACTIC EXTEND rules are now of type
+glob_tactic_expr, instead of glob_tactic_expr * tactic. Only the first
+component is kept, the second one can be obtained via
+Tacinterp.eval_tactic.
+
+** ARGUMENT EXTEND **
+
+It is now forbidden to use TYPED simultaneously with {RAW,GLOB}_TYPED
+in ARGUMENT EXTEND statements.
+
+** Renaming of rawconstr to glob_constr **
+
+The "rawconstr" type has been renamed to "glob_constr" for
+consistency. The "raw" in everything related to former rawconstr has
+been changed to "glob". For more details about the rationale and
+scripts to migrate code using Coq's internals, see commits 13743,
+13744, 13755, 13756, 13757, 13758, 13761 (by glondu, end of December
+2010) in Subversion repository. Contribs have been fixed too, and
+commit messages there might also be helpful for migrating.
+
+=========================================
 = CHANGES BETWEEN COQ V8.2 AND COQ V8.3 =
 =========================================