Mise en place des V8Notation et V8Infix pour declarer des notations en v8 meme si incompatible avec la syntaxe v7

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

3 files changed, 37 insertions, 18 deletions

diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v
index 3c4ed1e3c8..d0798eece7 100644
--- a/theories/ZArith/Zsyntax.v
+++ b/theories/ZArith/Zsyntax.v
@@ -12,6 +12,7 @@ Require Export fast_integer.
 Require Export zarith_aux.
 
 V7only[
+
 Grammar znatural ident :=
   nat_id [ prim:var($id) ] -> [$id]
 
@@ -224,10 +225,9 @@ Syntax constr
 .
 ].
 
-(* For parsing/printing based on scopes *)
 V7only[
+(* For parsing/printing based on scopes *)
 Module Z_scope.
-].
 
 Infix LEFTA 4 "+" Zplus : Z_scope.
 Infix LEFTA 4 "-" Zminus : Z_scope.
@@ -261,7 +261,6 @@ Notation "x <> y" := ~(eq Z x y) (at level 5, no associativity) : Z_scope.
 
 (* Notation "| x |" (Zabs x) : Z_scope.(* "|" conflicts with THENS *)*)
 
-V7only[
 (* Overwrite the printing of "`x = y`" *)
 Syntax constr level 0:
   Zeq [ (eq Z $n1 $n2) ] -> [[<hov 0> $n1 [1 0] "= " $n2 ]].
@@ -270,10 +269,3 @@ Open Scope Z_scope.
 
 End Z_scope.
 ].
-
-(* Declare Scope positive_scope with Key P. *)
-
-(*
-Arguments Scope POS [positive_scope].
-Arguments Scope NEG [positive_scope].
-*)
diff --git a/theories/ZArith/fast_integer.v b/theories/ZArith/fast_integer.v
index cb0a2b9935..165c26f148 100644
--- a/theories/ZArith/fast_integer.v
+++ b/theories/ZArith/fast_integer.v
@@ -23,21 +23,25 @@ Inductive positive : Set :=
 | xO : positive -> positive
 | xH : positive.
 
+(* Declare Scope positive_scope with Key P *)
 Delimits Scope positive_scope with P.
-Delimits Scope Z_scope with Z.
+
+(* Automatically open scope positive_scope for type positive, xO and xI *)
+Bind Scope positive_scope with positive.
 Arguments Scope xO [ positive_scope ].
 Arguments Scope xI [ positive_scope ].
 
 Inductive Z : Set := 
   ZERO : Z | POS : positive -> Z | NEG : positive -> Z.
 
-Bind Scope positive_scope with positive.
+(* Declare Scope positive_scope with Key Z *)
+Delimits Scope Z_scope with Z.
+
+(* Automatically open scope Z_scope for arguments of type Z, POS and NEG *)
 Bind Scope Z_scope with Z.
 Arguments Scope POS [ Z_scope ].
 Arguments Scope NEG [ Z_scope ].
 
-Section fast_integers.
-
 Inductive relation : Set := 
   EGAL :relation | INFERIEUR : relation | SUPERIEUR : relation.
 
@@ -86,7 +90,7 @@ with add_carry [x,y:positive]:positive :=
           end
   end.
 
-Infix LEFTA 4 "+" add : positive_scope.
+V8Infix "+" add : positive_scope.
 
 Open Scope positive_scope.
 
@@ -807,6 +811,8 @@ Definition Zplus := [x,y:Z]
              end
     end.
 
+V8Infix "+" Zplus : Z_scope.
+
 (** Opposite *)
 
 Definition Zopp := [x:Z]
@@ -816,6 +822,8 @@ Definition Zopp := [x:Z]
     | (NEG x) => (POS x)
     end.
 
+V8Notation "- x" := (Zopp x) : Z_scope.
+
 Theorem Zero_left: (x:Z) (Zplus ZERO x) = x.
 Proof.
 Induction x; Auto with arith.
@@ -1031,7 +1039,7 @@ Fixpoint times [x:positive] : positive -> positive:=
   | xH => y
   end.
 
-Infix LEFTA 3 "*" times : positive_scope.
+V8Infix "*" times : positive_scope.
 
 (** Correctness of multiplication on positive *)
 Theorem times_convert :
@@ -1076,7 +1084,7 @@ Definition Zmult := [x,y:Z]
              end
     end.
 
-Infix LEFTA 3 "*" Zmult : Z_scope.
+V8Infix "*" Zmult : Z_scope.
 
 Open Scope Z_scope.
 
@@ -1202,6 +1210,8 @@ Definition Zcompare := [x,y:Z]
              end
   end.
 
+V8Infix "?=" Zcompare (at level 50, no associativity) : Z_scope.
+
 Theorem Zcompare_EGAL : (x,y:Z) (Zcompare x y) = EGAL <-> x = y.
 Proof.
 Intros x y;Split; [
@@ -1471,7 +1481,6 @@ Intros x y;Case x;Case y; [
 | Unfold Zcompare; Intros q p; Rewrite <- ZC4; Intros H; Exists (true_sub q p);
   Simpl; Rewrite (ZC1 q p H); Trivial with arith].
 Qed.
-End fast_integers.
 
 V7only [
   Comments "Compatibility with the old version of times and times_convert".
diff --git a/theories/ZArith/zarith_aux.v b/theories/ZArith/zarith_aux.v
index 81c87f7c1d..c7fc10ee74 100644
--- a/theories/ZArith/zarith_aux.v
+++ b/theories/ZArith/zarith_aux.v
@@ -27,6 +27,22 @@ Definition Zgt := [x,y:Z](Zcompare x y) = SUPERIEUR.
 Definition Zle := [x,y:Z]~(Zcompare x y) = SUPERIEUR.
 Definition Zge := [x,y:Z]~(Zcompare x y) = INFERIEUR.
 
+V8Infix "<=" Zle : Z_scope.
+V8Infix "<"  Zlt : Z_scope.
+V8Infix ">=" Zge : Z_scope.
+V8Infix ">"  Zgt : Z_scope.
+
+V8Notation "x <= y <= z" := (Zle x y)/\(Zle y z)
+  (at level 50, y at next level):Z_scope.
+V8Notation "x <= y < z"  := (Zle x y)/\(Zlt y z)
+  (at level 50, y at next level):Z_scope.
+V8Notation  "x < y < z"  := (Zlt x y)/\(Zlt y z)
+  (at level 50, y at next level):Z_scope.
+V8Notation  "x < y <= z" := (Zlt x y)/\(Zle y z) 
+  (at level 50, y at next level):Z_scope.
+V8Notation  "x = y = z" := x=y/\y=z
+  (at level 50, y at next level) : Z_scope.
+
 (** Sign function *)
 Definition Zsgn [z:Z] : Z :=
   Cases z of 
@@ -668,6 +684,8 @@ Qed.
 
 Definition Zminus := [m,n:Z](Zplus m (Zopp n)).
 
+V8Infix "-" Zminus : Z_scope.
+
 Lemma Zminus_plus_simpl : 
   (n,m,p:Z)((Zminus n m)=(Zminus (Zplus p n) (Zplus p m))).