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

3 files changed, 4 insertions, 2 deletions

diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v
index bb3cfc5a8..ad1cc5cf1 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 31ca8f804..9d379548a 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 b7876130a..29feab5ca 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).