Ajout notation [ x ; ... ; y ] dans list_scope. Changement de la

syntaxe interne de ring_lookup et field_lookup qui n'était pas assez
robuste pour supporter une syntaxe [ ... ] dans constr.  
Déplacement de now_show de List.v vers Tactics.v, déplacement de "[ _ ]"
au niveau 0.



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

1 files changed, 3 insertions, 1 deletions

diff --git a/CHANGES b/CHANGES
index bf11db4680..2fd30d416b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -63,6 +63,7 @@ Libraries (DOC TO CHECK)
   elements, nothing more). 
 - In ListSet, a few definitions are now in Type (may induce a few
   incompatibilities).
+- Notation [t;...;u] for lists made available in list_scope.
 - Changes in FSets/FMaps:
   - Improvements: in particular FMap now provides an induction principle 
     on maps, and some properties about FSets and fold needs less hypotheses.
@@ -99,7 +100,8 @@ Notations, coercions and implicit arguments
   (DOC TODO?)
 - New options Global and Local to "Implicit Arguments" for section
   surviving or non export outside module.
-- Level "constr" moved from 9 to 8. (DOC TODO?)
+- Level "constr" moved from 9 to 8 and notation "[ _ ]" now at level 0
+  (easy to fix in case of incompatibilites). (DOC TODO?)
 - Structure/Record now printed as Record (unless option Printing All is set).
 - Support for parametric notations defining constants.
 - Insertion of coercions below product types refrains to unfold