From 701b613fd6f5e27cf69584171fb853cbf48f4530 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 12 Sep 2003 14:44:07 +0000
Subject: Bind et Delimit pour positive et Z (hors section)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4368 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/ZArith/Zsyntax.v      |  5 ++---
 theories/ZArith/fast_integer.v | 13 ++++++++++++-
 2 files changed, 14 insertions(+), 4 deletions(-)

(limited to 'theories/ZArith')

diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v
index 24fd54266c..3c4ed1e3c8 100644
--- a/theories/ZArith/Zsyntax.v
+++ b/theories/ZArith/Zsyntax.v
@@ -273,8 +273,7 @@ End Z_scope.
 
 (* Declare Scope positive_scope with Key P. *)
 
-Delimits Scope positive_scope with P.
-Delimits Scope Z_scope with Z.
-
+(*
 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 334dc050fb..cb0a2b9935 100644
--- a/theories/ZArith/fast_integer.v
+++ b/theories/ZArith/fast_integer.v
@@ -17,16 +17,27 @@ Require Mult.
 Require Minus.
 
 (** Definition of fast binary integers *)
-Section fast_integers.
 
 Inductive positive : Set :=
   xI : positive -> positive
 | xO : positive -> positive
 | xH : positive.
 
+Delimits Scope positive_scope with P.
+Delimits Scope Z_scope with Z.
+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.
+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.
 
-- 
cgit v1.2.3