reorganisation des niveaux (ex: = est a 70)

Hint Destruct: syntaxe similaire aux autres hints...


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

12 files changed, 62 insertions, 63 deletions

diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index e2ff55b231..984bd77c4f 100755
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -174,7 +174,7 @@ Definition negb := [b:bool]Cases b of
 
 Infix "||" orb  (at level 4, left associativity) : bool_scope.
 Infix "&&" andb (at level 3, no associativity) : bool_scope
-  V8only (at level 30, left associativity).
+  V8only (at level 40, left associativity).
 Notation "- b" := (negb b) : bool_scope V8only.
 
 Open Local Scope bool_scope.
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 680b1e20e5..4c284818bb 100755
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -126,19 +126,19 @@ Definition all := [A:Type][P:A->Prop](x:A)(P x).
 V7only [ Notation Ex  := (ex ?). ].
 Notation "'EX' x | p"      := (ex ? [x]p)
   (at level 10, p at level 8) : type_scope
-  V8only "'exists' x | p" (at level 200, x ident, p at level 80).
+  V8only "'exists' x | p" (at level 200, x ident, p at level 99).
 Notation "'EX' x : t | p"  := (ex ? [x:t]p)
   (at level 10, p at level 8) : type_scope
-  V8only "'exists' x : t | p" (at level 200, x ident, p at level 80).
+  V8only "'exists' x : t | p" (at level 200, x ident, p at level 99).
 
 V7only [ Notation Ex2 := (ex2 ?). ].
 Notation "'EX' x | p & q"       := (ex2 ? [x]p [x]q)
   (at level 10, p, q at level 8) : type_scope
-  V8only "'exists2' x | p & q" (at level 200, x ident, p, q at level 80).
+  V8only "'exists2' x | p & q" (at level 200, x ident, p, q at level 99).
 Notation "'EX' x : t | p & q"   := (ex2 ? [x:t]p [x:t]q)
   (at level 10, p, q at level 8) : type_scope
   V8only "'exists2' x : t | p & q"
-    (at level 200, x ident, t at level 200, p, q at level 80).
+    (at level 200, x ident, t at level 200, p, q at level 99).
 
 V7only [Notation All := (all ?).
 Notation "'ALL' x | p"     := (all ? [x]p)
diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v
index 102e67db62..f95f56d37f 100644
--- a/theories/Init/LogicSyntax.v
+++ b/theories/Init/LogicSyntax.v
@@ -24,17 +24,17 @@ Notation "'ALL' x : t | p" := (all ? [x:t]p) (at level 10, p at level 8)
 
 V7only [ Notation Ex  := (ex ?). ].
 Notation "'EX' x | p"      := (ex ? [x]p)    (at level 10, p at level 8)
-  V8only "'exists' x , p" (at level 200, x at level 80).
+  V8only "'exists' x , p" (at level 200, x at level 99).
 Notation "'EX' x : t | p"  := (ex ? [x:t]p)  (at level 10, p at level 8)
-  V8only "'exists' x : t , p" (at level 200, x at level 80).
+  V8only "'exists' x : t , p" (at level 200, x at level 99).
 
 V7only [ Notation Ex2 := (ex2 ?). ].
 Notation "'EX' x | p & q"       := (ex2 ? [x]p [x]q)
   (at level 10, p, q at level 8)
-  V8only "'exists2' x , p & q" (at level 200, x at level 80).
+  V8only "'exists2' x , p & q" (at level 200, x at level 99).
 Notation "'EX' x : t | p & q"   := (ex2 ? [x:t]p [x:t]q)
   (at level 10, p, q at level 8)
-  V8only "'exists2' x : t , p & q" (at level 200, x at level 80).
+  V8only "'exists2' x : t , p & q" (at level 200, x at level 99).
 
 V7only[
 (** Parsing only of things in [Logic.v] *)
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 8a107f5c08..149c757514 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -18,7 +18,7 @@ Uninterpreted Notation "x \/ y" (at level 7, right associativity).
 Uninterpreted Notation "x <-> y" (at level 8, right associativity).
 
 Uninterpreted Notation "~ x" (at level 5, right associativity)
-  V8only (at level 55, right associativity).
+  V8only (at level 75, right associativity).
 
 (** Notations for equality and inequalities *)
 
@@ -34,28 +34,28 @@ Uninterpreted Notation "x <> y  :> T"
 Uninterpreted Notation "x <> y"
   (at level 5, no associativity).
 
-Uninterpreted V8Notation "x <= y" (at level 50, no associativity).
-Uninterpreted V8Notation "x < y" (at level 50, no associativity).
-Uninterpreted V8Notation "x >= y" (at level 50, no associativity).
-Uninterpreted V8Notation "x > y" (at level 50, no associativity).
+Uninterpreted V8Notation "x <= y" (at level 70, no associativity).
+Uninterpreted V8Notation "x < y" (at level 70, no associativity).
+Uninterpreted V8Notation "x >= y" (at level 70, no associativity).
+Uninterpreted V8Notation "x > y" (at level 70, no associativity).
 
-Uninterpreted V8Notation "x <= y <= z" (at level 50, y at next level).
-Uninterpreted V8Notation "x <= y < z"  (at level 50, y at next level).
-Uninterpreted V8Notation "x < y < z"   (at level 50, y at next level).
-Uninterpreted V8Notation "x < y <= z"  (at level 50, y at next level).
+Uninterpreted V8Notation "x <= y <= z" (at level 70, y at next level).
+Uninterpreted V8Notation "x <= y < z"  (at level 70, y at next level).
+Uninterpreted V8Notation "x < y < z"   (at level 70, y at next level).
+Uninterpreted V8Notation "x < y <= z"  (at level 70, y at next level).
 
 (** Arithmetical notations (also used for type constructors) *)
 
 Uninterpreted Notation "x * y" (at level 3, right associativity)
-  V8only (at level 30, left associativity).
-Uninterpreted V8Notation "x / y" (at level 30, left associativity).
+  V8only (at level 40, left associativity).
+Uninterpreted V8Notation "x / y" (at level 40, left associativity).
 Uninterpreted Notation "x + y" (at level 4, left associativity).
 Uninterpreted Notation "x - y" (at level 4, left associativity).
-Uninterpreted Notation "- x" (at level 0) V8only (at level 40).
+Uninterpreted Notation "- x" (at level 0) V8only (at level 50).
 Uninterpreted Notation "/ x" (at level 0)
-  V8only (at level 30, left associativity).
+  V8only (at level 40, left associativity).
 
-Uninterpreted V8Notation "x ^ y" (at level 20, left associativity).
+Uninterpreted V8Notation "x ^ y" (at level 30, left associativity).
 
 (** Notations for pairs *)
 
@@ -68,38 +68,38 @@ Uninterpreted Notation "( x , y )" (at level 0)
 
 Uninterpreted Notation "B + { x : A | P }"
   (at level 4, left associativity, only parsing)
-  V8only (at level 40, x at level 80, left associativity, only parsing).
+  V8only (at level 50, x at level 99, left associativity, only parsing).
 
 Uninterpreted Notation "B + { x : A | P & Q }"
   (at level 4, left associativity, only parsing)
-  V8only (at level 40, x at level 80, left associativity, only parsing).
+  V8only (at level 50, x at level 99, left associativity, only parsing).
 
 Uninterpreted Notation "B + { x : A & P }"
   (at level 4, left associativity, only parsing)
-  V8only (at level 40, x at level 80, left associativity, only parsing).
+  V8only (at level 50, x at level 99, left associativity, only parsing).
 
 Uninterpreted Notation "B + { x : A & P & Q }"
   (at level 4, left associativity, only parsing)
-  V8only (at level 40, x at level 80, left associativity, only parsing).
+  V8only (at level 50, x at level 99, left associativity, only parsing).
 
 (* At level 1 to factor with {x:A|P} etc *)
 
 Uninterpreted Notation "{ A }  + { B }" (at level 1)
-  V8only (at level 0, A at level 80).
+  V8only (at level 0, A at level 99).
 
 Uninterpreted Notation "A + { B }" (at level 4, left associativity)
-  V8only (at level 40, B at level 80, left associativity).
+  V8only (at level 50, B at level 99, left associativity).
 
 (** Notations for sigma-types or subsets *)
 
 Uninterpreted Notation "{ x : A  |  P }" (at level 1)
-  V8only (at level 0, x at level 80).
+  V8only (at level 0, x at level 99).
 Uninterpreted Notation "{ x : A  |  P  &  Q }" (at level 1)
-  V8only (at level 0, x at level 80).
+  V8only (at level 0, x at level 99).
 
 Uninterpreted Notation "{ x : A  &  P }" (at level 1)
-  V8only (at level 0, x at level 80).
+  V8only (at level 0, x at level 99).
 Uninterpreted Notation "{ x : A  &  P  &  Q }" (at level 1)
-  V8only (at level 0, x at level 80).
+  V8only (at level 0, x at level 99).
 
 Delimits Scope type_scope with T.
diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v
index 4168655fea..50b203d4e5 100644
--- a/theories/Lists/PolyList.v
+++ b/theories/Lists/PolyList.v
@@ -20,7 +20,7 @@ Set Implicit Arguments.
 Inductive list : Set := nil : list | cons : A -> list -> list.
 
 Infix "::" cons (at level 7, right associativity) : list_scope
-  V8only (at level 45, right associativity).
+  V8only (at level 60, right associativity).
 
 Open Scope list_scope.
 
@@ -44,7 +44,7 @@ Fixpoint app [l:list] : list -> list
                  end.
 
 Infix RIGHTA 7 "^" app : list_scope
-  V8only RIGHTA 45 "++".
+  V8only RIGHTA 60 "++".
 
 Lemma app_nil_end : (l:list)l=(l^nil).
 Proof. 
@@ -635,8 +635,8 @@ V7only [Implicits nil [].].
 
 (** Exporting list notations *)
 
-V8Infix "::" cons (at level 45, right associativity) : list_scope.
+V8Infix "::" cons (at level 60, right associativity) : list_scope.
 
-Infix RIGHTA 7 "^" app : list_scope V8only RIGHTA 45 "++".
+Infix RIGHTA 7 "^" app : list_scope V8only RIGHTA 60 "++".
 
 Open Scope list_scope.
diff --git a/theories/Num/NSyntax.v b/theories/Num/NSyntax.v
index 55912fdda5..00d7a032d4 100644
--- a/theories/Num/NSyntax.v
+++ b/theories/Num/NSyntax.v
@@ -10,12 +10,12 @@
 
 Require Export Params.
 
-Infix 6 "<" lt V8only 50.
-Infix 6 "<=" le V8only 50.
-Infix 6 ">" gt V8only 50.
-Infix 6 ">=" ge V8only 50.
+Infix 6 "<" lt V8only 70.
+Infix 6 "<=" le V8only 70.
+Infix 6 ">" gt V8only 70.
+Infix 6 ">=" ge V8only 70.
 
-(*i Infix 7 "+" plus V8only 40. i*)
+(*i Infix 7 "+" plus V8only 50. i*)
 
 Grammar constr lassoc_constr4 :=
   squash_sum
diff --git a/theories/Num/NeqDef.v b/theories/Num/NeqDef.v
index 0e00294223..ff5bc3e67c 100644
--- a/theories/Num/NeqDef.v
+++ b/theories/Num/NeqDef.v
@@ -15,7 +15,7 @@ Require EqParams.
 Require EqAxioms.
 
 Definition neq : N -> N -> Prop := [x,y] ~(x=y).
-Infix 6 "<>" neq V8only 50.
+Infix 6 "<>" neq V8only 70.
 
 (* Proofs of axioms *)
 Lemma eq_not_neq : (x,y:N)x=y->~(x<>y).
diff --git a/theories/Num/NeqParams.v b/theories/Num/NeqParams.v
index 7f7a5139e4..4b76771669 100644
--- a/theories/Num/NeqParams.v
+++ b/theories/Num/NeqParams.v
@@ -15,7 +15,7 @@ Require Export Params.
 
 Parameter neq : N -> N -> Prop.
 
-Infix 6 "<>" neq V8only 50.
+Infix 6 "<>" neq V8only 70.
 
 
 
diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v
index 88fd935b10..b8c5c2f4c3 100644
--- a/theories/Reals/Ranalysis1.v
+++ b/theories/Reals/Ranalysis1.v
@@ -35,7 +35,7 @@ V8Infix "-" minus_fct : Rfun_scope.
 V8Infix "/" div_fct : Rfun_scope.
 Notation Local "f1 'o' f2" := (comp f1 f2) (at level 2, right associativity)
   : Rfun_scope 
-  V8only (at level 15, right associativity).
+  V8only (at level 20, right associativity).
 V8Notation "/ x" := (inv_fct x) : Rfun_scope.
 
 Delimits Scope Rfun_scope with F.
diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v
index 95d60efebe..3929acdf9f 100644
--- a/theories/Reals/Rsyntax.v
+++ b/theories/Reals/Rsyntax.v
@@ -210,33 +210,32 @@ Infix "<"  Rlt (at level 5, no associativity) : R_scope.
 Infix ">=" Rge (at level 5, no associativity) : R_scope.
 Infix ">" Rgt (at level 5, no associativity) : R_scope.
 Infix "+" Rplus (at level 4) : R_scope
-  V8only (at level 40, left associativity).
+  V8only (at level 50, left associativity).
 Infix "-" Rminus (at level 4) : R_scope
-  V8only (at level 40, left associativity).
+  V8only (at level 50, left associativity).
 Infix "*" Rmult (at level 3) : R_scope
-  V8only (at level 30, left associativity).
+  V8only (at level 40, left associativity).
 Infix "/" Rdiv (at level 3) : R_scope
-  V8only (at level 30, left associativity).
-Notation "- x" := (Ropp x) (at level 0) : R_scope
   V8only (at level 40, left associativity).
+Notation "- x" := (Ropp x) (at level 0) : R_scope
+  V8only (at level 50, left associativity).
 Notation "x == y == z" := (eqT R x y)/\(eqT R y z)
   (at level 5, y at level 4, no associtivity): R_scope
-  V8only "x = y = z" (at level 50, y at next level, no associativity).
+  V8only "x = y = z" (at level 70, y at next level, no associativity).
 Notation "x <= y <= z" := (Rle x y)/\(Rle y z)
   (at level 5, y at level 4) : R_scope
-  V8only (at level 50, y at next level, no associativity).
+  V8only (at level 70, y at next level, no associativity).
 Notation "x <= y < z" := (Rle x y)/\(Rlt y z)
   (at level 5, y at level 4) : R_scope
-  V8only (at level 50, y at next level, no associativity).
+  V8only (at level 70, y at next level, no associativity).
 Notation "x < y < z" := (Rlt x y)/\(Rlt y z)
   (at level 5, y at level 4) : R_scope
-  V8only (at level 50, y at next level, no associativity).
+  V8only (at level 70, y at next level, no associativity).
 Notation "x < y <= z" := (Rlt x y)/\(Rle y z)
   (at level 5, y at level 4) : R_scope
-  V8only (at level 50, y at next level, no associativity).
-(*Notation "x <> y" := ~(eqT R x y) (at level 5) : R_scope.*)
+  V8only (at level 70, y at next level, no associativity).
 Notation "/ x" := (Rinv x) (at level 0): R_scope
-  V8only (at level 30, left associativity).
+  V8only (at level 40, left associativity).
 
 Open Local Scope R_scope.
 End R_scope.
diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v
index d5055507b4..2805406a34 100644
--- a/theories/ZArith/Zsyntax.v
+++ b/theories/ZArith/Zsyntax.v
@@ -240,18 +240,18 @@ Infix NONA 5 ">"  Zgt  : Z_scope.
 Infix NONA 5 "?=" Zcompare : Z_scope.
 Notation "x <= y <= z" := (Zle x y)/\(Zle y z)
   (at level 5, y at level 4):Z_scope
-  V8only (at level 50, y at next level).
+  V8only (at level 70, y at next level).
 Notation "x <= y < z"  := (Zle x y)/\(Zlt y z)
   (at level 5, y at level 4):Z_scope
-  V8only (at level 50, y at next level).
+  V8only (at level 70, y at next level).
 Notation  "x < y < z"  := (Zlt x y)/\(Zlt y z)
   (at level 5, y at level 4):Z_scope
-  V8only (at level 50, y at next level).
+  V8only (at level 70, y at next level).
 Notation  "x < y <= z" := (Zlt x y)/\(Zle y z)
   (at level 5, y at level 4):Z_scope
-  V8only (at level 50, y at next level).
+  V8only (at level 70, y at next level).
 Notation  "x = y = z" := x=y/\y=z : Z_scope
-  V8only (at level 50, y at next level).
+  V8only (at level 70, y at next level).
 
 (* Now a polymorphic notation
 Notation "x <> y" := ~(eq Z x y) (at level 5, no associativity) : Z_scope.
diff --git a/theories/ZArith/fast_integer.v b/theories/ZArith/fast_integer.v
index 68d80e8905..43be524191 100644
--- a/theories/ZArith/fast_integer.v
+++ b/theories/ZArith/fast_integer.v
@@ -1537,7 +1537,7 @@ Definition Zcompare := [x,y:Z]
   | (NEG x') (NEG y') => (Op (compare x' y' EGAL))
   end.
 
-V8Infix "?=" Zcompare (at level 50, no associativity) : Z_scope.
+V8Infix "?=" Zcompare (at level 70, no associativity) : Z_scope.
 
 Open Local Scope Z_scope.