From 7d9d5157df272f6b276f3271cafd02d2488bae05 Mon Sep 17 00:00:00 2001
From: glondu
Date: Fri, 11 Feb 2011 15:30:19 +0000
Subject: Update changelogs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13834 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES             |  3 +++
 dev/doc/changes.txt | 15 +++++++++++++++
 2 files changed, 18 insertions(+)

diff --git a/CHANGES b/CHANGES
index 0f42648221..325490969e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -15,6 +15,7 @@ Changes from V8.3 to V8.4
 Tactics
 
 - New tactics constr_eq, is_evar and has_evar.
+- Remove the two-argument variant of "decide equality".
 
 Vernacular commands
 
@@ -22,6 +23,7 @@ Vernacular commands
 - When the output file of "Print Universes" ends in ".dot" or ".gv",
   the universe graph is printed in the DOT language, and can be
   processed by Graphviz tools.
+- New command "Print Sorted Universes".
 - The undocumented and obsolete option "Set/Unset Boxed Definitions" has
   been removed, as well as syntaxes like "Boxed Fixpoint foo".
 
@@ -59,6 +61,7 @@ Libraries
   All old names change: functions' name become the CaML one and for example
   Vcons become Vector.cons. You can use notations by importing
   Vector.VectorNotations.
+- Removal of TheoryList. Requiring List instead should work most of the time.
 
 Internal infrastructure
 
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 3953623885..035b3ad245 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -20,6 +20,21 @@ 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 =
 =========================================
-- 
cgit v1.2.3