MAJ

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5591 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 1 deletions

diff --git a/CHANGES b/CHANGES
index cdedac16e..3a1391ffd 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,7 +1,7 @@
 Changes from V8.0beta to V8.0
 =============================
 
-Commands
+Vernacular commands
 
 - New option "Set Printing All" to deactivate all high-level forms of
   printing (implicit arguments, coercions, destructing let,
@@ -13,6 +13,13 @@ Commands
 - Command "Print." discontinued.
 - Redundant syntax "Implicit Arguments On/Off" discontinued
 
+Syntax
+
+- Semantic change of the if-then-else construction: "if c then t1 else t2"
+  now stands for "match c with c1 _ ... _ => t1 | c2 _ ... _ => t2 end"
+  with no dependency of t1 and t2 in the arguments of the constructors;
+  this may cause incompatibilities for files translated using coq 8.0beta
+
 Interpretation scopes
 
 - Delimiting key %bool for bool_scope added
@@ -28,6 +35,10 @@ Tactic Language
 
 - Intro patterns now supported in Ltac (parsed with prefix "ipattern:")
 
+Commands
+
+- Added option -top to change the name of the toplevel module "Top"
+
 Tools
 
 - Coqdoc updated to new syntax and now part of Coq sources