Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; améliorations diverses de l'affichage; affinement de la syntaxe et des options de Notation; branchement de Syntactic Definition sur Notation

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

1 files changed, 9 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 5be095ab8e..e3393dc6e1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -14,6 +14,8 @@ Symbolic notations
 
 - Introduction of a notion of scope gathering notations in a consistent set;
   set a notation sets has been developped for nat, Z and R
+- New command "Notation" for declaring notations simultaneously for
+  parsing and printing
 - Declarations with only implicit arguments now handled (e.g. the
   argument of nil can be set implicit; use !nil to refer to nil
   without arguments)
@@ -25,6 +27,10 @@ Library
 - Lemmas in Set from Compare_dec.v (le_lt_dec, ...) and Wf_nat.v
   (lt_wf_rec, ...) are now transparent. This may be source of
   incompatibilities.
+- Syntactic Definitions Fst, Snd, Ex, All, Ex2, AllT, ExT, ExT2,
+  ProjS1, ProjS2, Error, Value and Except are turned to
+  notations. They now must be applied (incompatibilities only in
+  unrealistic cases).
 
 Language
 
@@ -74,10 +80,13 @@ Tactics
   hypothesis was unfolded to `x < y` -> False. This is fixed. In addition,
   it can also recognize 'False' in the hypothesis and use it to solve the
   goal.
+- New syntax for Ring and Field when arguments are provided (use "Ring on" and
+  "Field on")
 
 Miscellaneous
 
 - Printing Coercion now used through the standard keywords Set/Add, Test, Print
+- "Print Term id" is an alias for "Print id"
 
 Incompatibilities