Backtrack sur la mise à disposition en standard de la notation [ x ; ... ; y ]

pour les listes (trop contraignant)


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

6 files changed, 5 insertions, 10 deletions

diff --git a/CHANGES b/CHANGES
index 53ca78118e..0fd8c3ac68 100644
--- a/CHANGES
+++ b/CHANGES
@@ -105,8 +105,7 @@ Notations, coercions, implicit arguments and type inference
   (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 and notation "[ _ ]" now reserved at level 0
-  (may need to move post-fixed uses of [ ] at level 8). (DOC TODO?)
+- Level "constr" moved from 9 to 8. (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
diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v
index bb3cfc5a8a..ad1cc5cf10 100644
--- a/contrib/ring/Ring_normalize.v
+++ b/contrib/ring/Ring_normalize.v
@@ -897,6 +897,6 @@ End rings.
 Infix "+" := Pplus : ring_scope.
 Infix "*" := Pmult : ring_scope.
 Notation "- x" := (Popp x) : ring_scope.
-Notation "[ x ]" := (Pvar x) : ring_scope.
+Notation "[ x ]" := (Pvar x) (at level 0) : ring_scope.
 
 Delimit Scope ring_scope with ring.
diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v
index 31ca8f8049..9d379548a6 100644
--- a/contrib/romega/ReflOmegaCore.v
+++ b/contrib/romega/ReflOmegaCore.v
@@ -879,7 +879,7 @@ Infix "+" := Tplus : romega_scope.
 Infix "*" := Tmult : romega_scope.
 Infix "-" := Tminus : romega_scope.
 Notation "- x" := (Topp x) : romega_scope.
-Notation "[ x ]" := (Tvar x) : romega_scope.
+Notation "[ x ]" := (Tvar x) (at level 0) : romega_scope.
 
 (* \subsubsection{Definition of reified goals} *)
 
diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v
index b7876130a4..29feab5cab 100644
--- a/contrib/setoid_ring/Ring_theory.v
+++ b/contrib/setoid_ring/Ring_theory.v
@@ -19,6 +19,8 @@ Reserved Notation "x -! y" (at level 50, left associativity).
 Reserved Notation "x *! y" (at level 40, left associativity).
 Reserved Notation "-! x" (at level 35, right associativity).
 
+Reserved Notation "[ x ]" (at level 0).
+
 Reserved Notation "x ?== y" (at level 70, no associativity).
 Reserved Notation "x -- y" (at level 50, left associativity).
 Reserved Notation "x ** y" (at level 40, left associativity).
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 0aee1d4ca7..9a0406d591 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -71,8 +71,6 @@ Reserved Notation "{ x : A  |  P  &  Q }" (at level 0, x at level 99).
 Reserved Notation "{ x : A  &  P }" (at level 0, x at level 99).
 Reserved Notation "{ x : A  &  P  &  Q }" (at level 0, x at level 99).
 
-Reserved Notation "[ x ]" (at level 0).
-
 Delimit Scope type_scope with type.
 Delimit Scope core_scope with core.
 
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 2cce009a27..f1bcc792d6 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -82,10 +82,6 @@ Implicit Arguments nil [A].
 Infix "::" := cons (at level 60, right associativity) : list_scope.
 Infix "++" := app (right associativity, at level 60) : list_scope.
 
-Notation "[ ]" := nil : list_scope.
-Notation "[ x ]" := (cons x nil) : list_scope.
-Notation "[ x ; y ; .. ; z ]" := (cons x (cons y .. (cons z nil) .. )) : list_scope.
- 
 Open Scope list_scope.
 
 Delimit Scope list_scope with list.