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

6 files changed, 84 insertions, 33 deletions

diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 2df522988..eaa9256e5 100755
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -85,6 +85,8 @@ Fixpoint plus [n:nat] : nat -> nat :=
 Hint eq_plus : v62 := Resolve (f_equal2 nat nat nat plus).
 Hint eq_nat_binary : core := Resolve (f_equal2 nat nat).
 
+V8Infix "+" plus : nat_scope.
+
 Lemma plus_n_O : (n:nat) n=(plus n O).
 Proof.
   NewInduction n ; Simpl ; Auto.
@@ -114,6 +116,8 @@ Fixpoint  mult [n:nat] : nat -> nat :=
                | (S p) => (plus m (mult p m)) end.
 Hint eq_mult : core v62 := Resolve (f_equal2 nat nat nat mult).
 
+V8Infix "*" mult : nat_scope.
+
 Lemma mult_n_O : (n:nat) O=(mult n O).
 Proof.
   NewInduction n; Simpl; Auto.
@@ -137,6 +141,8 @@ Fixpoint minus [n:nat] : nat -> nat :=
          | (S k) (S l) => (minus k l)
         end. 
 
+V8Infix "-" minus : nat_scope.
+
 (** Definition of the usual orders, the basic properties of [le] and [lt] 
     can be found in files Le and Lt *)
 
@@ -146,18 +152,26 @@ Inductive le [n:nat] : nat -> Prop
     := le_n : (le n n)
      | le_S : (m:nat)(le n m)->(le n (S m)).
 
+V8Infix "<=" le : nat_scope.
+
 Hint constr_le : core v62 := Constructors le.
 (*i equivalent to : "Hints Resolve le_n le_S : core v62." i*)
 
 Definition lt := [n,m:nat](le (S n) m).
 Hints Unfold lt : core v62.
 
+V8Infix "<" lt : nat_scope.
+
 Definition ge := [n,m:nat](le m n).
 Hints Unfold ge : core v62.
 
+V8Infix ">=" ge : nat_scope.
+
 Definition gt := [n,m:nat](lt m n).
 Hints Unfold gt : core v62.
 
+V8Infix ">" gt : nat_scope.
+
 (** Pattern-Matching on natural numbers *)
 
 Theorem nat_case : (n:nat)(P:nat->Prop)(P O)->((m:nat)(P (S m)))->(P n).
@@ -187,15 +201,12 @@ Syntax constr
 (* For parsing/printing based on scopes *)
 V7only [
 Module nat_scope.
-].
-Infix 4 "+" plus : nat_scope V8only (left associativity).
-Infix 4 "-" minus : nat_scope V8only (left associativity).
-Infix 3 "*" mult : nat_scope V8only (left associativity).
+Infix 4 "+" plus : nat_scope.
+Infix 3 "*" mult : nat_scope.
+Infix 4 "-" minus : nat_scope.
 Infix NONA 5 "<=" le : nat_scope.
 Infix NONA 5 "<" lt : nat_scope.
 Infix NONA 5 ">=" ge : nat_scope.
 Infix NONA 5 ">" gt : nat_scope.
-
-V7only [
 End nat_scope.
 ].
diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
index 26857c81f..42a15c031 100644
--- a/theories/Reals/Rdefinitions.v
+++ b/theories/Reals/Rdefinitions.v
@@ -18,7 +18,10 @@ Require Export TypeSyntax.
 
 Parameter R:Type.
 
+(* Declare Scope positive_scope with Key R *)
 Delimits Scope R_scope with R.
+
+(* Automatically open scope R_scope for arguments of type R *)
 Bind Scope R_scope with R.
 
 Parameter R0:R.
@@ -30,6 +33,13 @@ Parameter Rinv:R->R.
 Parameter Rlt:R->R->Prop.    
 Parameter up:R->Z.
 
+V8Infix "+" Rplus : R_scope.
+V8Infix "*" Rmult : R_scope.
+V8Notation "- x" := (Ropp x) : R_scope.
+V8Notation "/ x" := (Rinv x) : R_scope.
+
+V8Infix "<"  Rlt : R_scope.
+
 (*i*******************************************************i*)
 
 (**********)
@@ -47,4 +57,22 @@ Definition Rminus:R->R->R:=[r1,r2:R](Rplus r1 (Ropp r2)).
 (**********)
 Definition Rdiv:R->R->R:=[r1,r2:R](Rmult r1 (Rinv r2)).
 
+V8Infix "-" Rminus : R_scope.
+V8Infix "/" Rdiv : R_scope.
+
+V8Infix "<=" Rle : R_scope.
+V8Infix ">=" Rge : R_scope.
+V8Infix ">" Rgt : R_scope.
+
+V8Notation "x = y = z" := (eqT R x y)/\(eqT R y z)
+  (at level 50, y at next level, no associativity) : R_scope.
+V8Notation "x <= y <= z" := (Rle x y)/\(Rle y z)
+  (at level 50, y at next level, no associativity) : R_scope.
+V8Notation "x <= y < z" := (Rle x y)/\(Rlt y z)
+  (at level 50, y at next level, no associativity) : R_scope.
+V8Notation "x < y < z" := (Rlt x y)/\(Rlt y z)
+  (at level 50, y at next level, no associativity) : R_scope.
+V8Notation "x < y <= z" := (Rlt x y)/\(Rle y z)
+  (at level 50, y at next level, no associativity) : R_scope.
+
 Hints Unfold Rgt : real.
diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v
index 771d89852..cf0d8ca46 100644
--- a/theories/Reals/Rsyntax.v
+++ b/theories/Reals/Rsyntax.v
@@ -200,11 +200,9 @@ Syntax constr
   | Rodd_inside [<<(REXPR <<(Rplus R1 $r)>>)>>] -> [ $r:"r_printer_odd" ]
   | Reven_inside [<<(REXPR <<(Rmult (Rplus R1 R1) $r)>>)>>] -> [ $r:"r_printer_even" ]
 .
-].
+
 (* For parsing/printing based on scopes *)
-V7only [
 Module R_scope.
-].
 
 Infix "<=" Rle (at level 5, no associativity) : R_scope.
 Infix "<"  Rlt (at level 5, no associativity) : R_scope.
@@ -222,7 +220,7 @@ Notation "- x" := (Ropp x) (at level 0) : R_scope
   V8only (at level 40, 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 (at level 50, y at next level, no associativity).
+  V8only "x = y = z" (at level 50, 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).
@@ -239,11 +237,6 @@ Notation "x < y <= z" := (Rlt x y)/\(Rle y z)
 Notation "/ x" := (Rinv x) (at level 0): R_scope
   V8only (at level 30, left associativity).
 
-V7only [
 Open Local Scope R_scope.
 End R_scope.
 ].
-
-(*
-Arguments Scope up [R_scope].
-*)
diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v
index 3c4ed1e3c..d0798eece 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 cb0a2b993..165c26f14 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 81c87f7c1..c7fc10ee7 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))).