MAJ

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

1 files changed, 13 insertions, 2 deletions

diff --git a/CHANGES b/CHANGES
index fd702addd8..9972e5810a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -5,8 +5,7 @@ A revision of the standard library and of concrete syntax of Coq, including
 
 - a completely new syntax for terms
 - renaming of various standard notions from French to English (esp in ZArith)
-- all notions of the standard library are declared with (strict)
-  implicit arguments
+- notions of the standard library are declared with (strict) implicit arguments
 - eq merged with eqT: old eq disappear, new eq (written =) is old eqT
   and new eqT is syntactic sugar for new eq (notation == is an alias
   for = and is written as it)
@@ -19,12 +18,20 @@ Vernacular commands
 - "Set Printing Width n" added, allows to change the size of width printing
    (TODO : doc).
 - "Implicit Variables Type x,y:t" assigns default types for binding variables.
+- "Set Implicits Printing" disable printing of implicit arguments
 
 Gallina
 
 - New syntax of the form "Inductive bool : Set := true, false : bool." for
   enumerated types
 
+Implicit arguments
+
+- Inductive in sections declared with implicits now "discharged" with
+  implicits (like constants and variables)
+- Set Implicit Arguments is strict by default in new syntax
+- Implicit Arguments flags are now synchronous with reset
+
 Grammar extensions
 
 - UTF-8 encoded unicode blocks 0380-03FF (greek letters) and 2100-214F
@@ -36,6 +43,10 @@ Grammar extensions
 Tactic language
 
 - Fail tactic now accepts a failure message
+- Fail levels are now decremented at "Match Context" blocks only and
+  if the right-hand-side of "Match term With" are tactics, these
+  tactics are never evaluated immediately and do not induce
+  backtracking (in contrast with "Match Context")
 
 Bugs