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

2 files changed, 30 insertions, 9 deletions

diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
index 26857c81f1..42a15c0318 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 771d898520..cf0d8ca46e 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].
-*)