MAJ

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

1 files changed, 21 insertions, 10 deletions

diff --git a/CHANGES b/CHANGES
index 585f204e7..6c6962ebc 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,20 +1,31 @@
-TODO: classer les changements intervenus entre la V7.0 beta et la V7.0
+TODO: classer les changements intervenus entre la V7.0 beta et la V7.0 ?
+et ceux intervenus entre la V6.3.1 et la V7.0beta ? Ou laisser des
+listes séparées ?
 
 Changes from V7.0 to V7.1
 -------------------------
 
-Note: items followed by (*) are sources of incompatibilities
+Notes:
+- items followed by (*) are sources of incompatibilities
+- items followed by (+) have been introduced in version 7.0
+
 
 Language
 
 - New reduction flags Zeta and Evar in Eval Compute, for inlining of
   local definitions and instantiation of existential variables
 - Delta reduction flag does not perform Zeta and Evar reduction any more (*)
+- new visibility discipline for Remark, Fact and Local: Remark's and
+  Fact's now survive at the end of section, but are only accessible using a
+  qualified names as soon as their strength expires; Local's disappear and
+  are moved into local definitions for each construction persistent at
+  section closing
 
 - known Coercion bugs fixed
 - Cases predicate inference bug fixed
 - known dependent Cases predicate bugs fixed
 
+
 Language : long names
 
 - Each construction has a unique absolute names built from a base
@@ -25,7 +36,7 @@ Language : long names
   by the module name (and possibly by a directory name, and so
   on). A fully qualified name is an absolute name which always refer
   to the the construction it denotes (to preserve the visibility of
-  all constructions, no conflict is allowed for an absolute name)
+  all constructions, no conflict is allowed for an absolute name) (+)
 - Long names are available for modules with the possibility of using
   the directory name as a component of the module full name (with
   option -R to coqtop and coqc, or command Add LoadPath)
@@ -61,15 +72,15 @@ Efficiency
 
 Parsing and grammar extension
 
-- Un lieur multiple comme (a:A)(a,b,c:(P a))(Q a), n'est plus compris comme
-  (a:A)(a0:(P a))(b:(P a),c:(P a))(Q a0), mais comme 
-  (a:A)(a0:(P a))(b:(P a0),c:(P a0))(Q a0) (*)
+- Un lieur multiple comme (a:A)(a,b:(P a))(Q a), n'est plus compris comme
+  (a:A)(a0:(P a))(b:(P a))(Q a0), mais comme 
+  (a:A)(a0:(P a))(b:(P a0))(Q a0)  (*)(+)
 - More constraints when writing ast 
-  - "{...}" and the macros $LIST, $VAR, etc. now expect a
-    metavariable (starting with $)
+  - "{...}" and the macros $LIST, $VAR, etc. now expect a metavariable
+    (an identifier starting with $) (*)
   - identifiers should starts with a letter or "_" and be followed
      by letters, digits, "_" or "'" (other caracters are still
-     supported but it is not advised to use them)
+     supported but it is not advised to use them) (*)(+)
 
 
 Commands
@@ -85,7 +96,7 @@ Standard library
 - New library on maps on integer (IntMap, contributed by Jean Goubault)
 - New lemmas about integer numbers [ZArith]
 - New lemmas about [Reals]
-- Exc/Error/Value renamed into Option/Some/None
+- Exc/Error/Value renamed into Option/Some/None (*)
 
 
 New user contributions