Notations

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

1 files changed, 17 insertions, 0 deletions

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 222f6de2f..4d3d30f21 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -15,6 +15,17 @@ Require BinPos.
 
 Inductive entier: Set := Nul : entier | Pos : positive -> entier.
 
+(** Declare binding key for scope positive_scope *)
+
+Delimits Scope N_scope with N.
+
+(** Automatically open scope N_scope for the constructors of N *)
+
+Bind Scope N_scope with entier.
+Arguments Scope Pos [ N_scope ].
+
+Open Local Scope N_scope.
+
 (** Operation x -> 2*x+1 *)
 
 Definition Un_suivi_de := [x]
@@ -39,6 +50,8 @@ Definition Nplus := [n,m]
   | (Pos p) (Pos q) => (Pos (add p q))
   end.
 
+V8Infix "+" Nplus : N_scope.
+
 (** Multiplication *)
 
 Definition Nmult := [n,m]
@@ -48,6 +61,8 @@ Definition Nmult := [n,m]
   | (Pos p) (Pos q) => (Pos (times p q))
   end.
 
+V8Infix "*" Nmult : N_scope.
+
 (** Order *)
 
 Definition Ncompare := [n,m]
@@ -58,6 +73,8 @@ Definition Ncompare := [n,m]
   | (Pos n') (Pos m') => (compare n' m' EGAL)
   end.
 
+V8Infix "?=" Ncompare (at level 70, no associativity) : N_scope.
+
 (** Peano induction on binary natural numbers *)
 
 Theorem Nind : (P:(entier ->Prop))