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

1 files changed, 28 insertions, 0 deletions

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.