From 629debcf068ffc4adc22bfc9a4b67251017525a0 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 6 Jul 2012 17:07:36 +0000
Subject: BinPos/BinInt/BinNat : fix some argument scopes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15540 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/NArith/BinNat.v | 8 ++++----
 theories/PArith/BinPos.v | 3 +--
 theories/ZArith/BinInt.v | 8 ++++----
 3 files changed, 9 insertions(+), 10 deletions(-)

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 046670f7b1..a42e39a252 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -893,11 +893,11 @@ Qed.
 
 (** Instantiation of generic properties of natural numbers *)
 
-Include NProp
- <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
+(** The Bind Scope prevents N to stay associated with abstract_scope.
+    (TODO FIX) *)
 
-(** Otherwise N stays associated with abstract_scope : (TODO FIX) *)
-Bind Scope N_scope with N.
+Include NProp. Bind Scope N_scope with N.
+Include UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
 
 (** In generic statements, the predicates [lt] and [le] have been
   favored, whereas [gt] and [ge] don't even exist in the abstract
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 58fe090dd6..a6c4ef54c1 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -1484,8 +1484,7 @@ Qed.
 
 (** We hence obtain all the generic properties of [min] and [max]. *)
 
-Include !UsualMinMaxLogicalProperties.
-Include !UsualMinMaxDecProperties.
+Include UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
 
 (** Minimum, maximum and constant one *)
 
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index a5c8affe7c..c3caed8724 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1153,11 +1153,11 @@ Program Definition rem_wd : Proper (eq==>eq==>eq) rem := _.
 Program Definition pow_wd : Proper (eq==>eq==>eq) pow := _.
 Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _.
 
-Include ZProp
- <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
+(** The Bind Scope prevents Z to stay associated with abstract_scope.
+    (TODO FIX) *)
 
-(** Otherwise Z stays associated with abstract_scope : (TODO FIX) *)
-Bind Scope Z_scope with Z.
+Include ZProp. Bind Scope Z_scope with Z.
+Include UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
 
 (** In generic statements, the predicates [lt] and [le] have been
   favored, whereas [gt] and [ge] don't even exist in the abstract
-- 
cgit v1.2.3