More dynamic argument scopes

 When arguments scopes are set manually, nothing new, they stay
 as they are (until maybe another Arguments invocation).
 But when argument scopes are computed out of the argument type and
 the Bind Scope information, this kind of scope is now dynamic:
 a later Bind Scope will be able to impact the scopes of an earlier
 constant. For Instance:

 Definition f (n:nat) := n.
 About f. (* Argument scope is [nat_scope] *)
 Bind Scope other_scope with nat.
 About f. (* Argument scope is [other_scope] *)

 This allows to get rid of hacks for modifying scopes during functor
 applications. Moreover, the subst_arguments_scope is now
 environment-insensitive (needed for forthcoming changes in declaremods).

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

11 files changed, 22 insertions, 42 deletions

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 5b1e83e6c..61a77bf0e 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -893,11 +893,9 @@ Qed.
 
 (** Instantiation of generic properties of natural numbers *)
 
-(** The Bind Scope prevents N to stay associated with abstract_scope.
-    (TODO FIX) *)
-
-Include NProp. Bind Scope N_scope with N.
-Include UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
+Include NProp
+ <+ UsualMinMaxLogicalProperties
+ <+ UsualMinMaxDecProperties.
 
 (** In generic statements, the predicates [lt] and [le] have been
   favored, whereas [gt] and [ge] don't even exist in the abstract
@@ -983,6 +981,8 @@ Qed.
 
 End N.
 
+Bind Scope N_scope with N.t N.
+
 (** Exportation of notations *)
 
 Infix "+" := N.add : N_scope.
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index a56f90b08..eca97ace9 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -26,15 +26,13 @@ Require Import ZProperties ZDivFloor ZSig ZSigZAxioms ZMake.
 
 Delimit Scope bigZ_scope with bigZ.
 
-Module BigZ <: ZType <: OrderedTypeFull <: TotalOrder.
- Include ZMake.Make BigN [scope abstract_scope to bigZ_scope].
- Bind Scope bigZ_scope with t t_.
- Include ZTypeIsZAxioms
+Module BigZ <: ZType <: OrderedTypeFull <: TotalOrder :=
+ ZMake.Make BigN
+ <+ ZTypeIsZAxioms
  <+ ZProp [no inline]
  <+ HasEqBool2Dec [no inline]
  <+ MinMaxLogicalProperties [no inline]
  <+ MinMaxDecProperties [no inline].
-End BigZ.
 
 (** For precision concerning the above scope handling, see comment in BigN *)
 
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 180fe0a96..28c298dbe 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -29,8 +29,6 @@ Module Make (NN:NType) <: ZType.
 
  Definition t := t_.
 
- Bind Scope abstract_scope with t t_.
-
  Definition zero := Pos NN.zero.
  Definition one  := Pos NN.one.
  Definition two := Pos NN.two.
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 62b148294..f073cae89 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -12,11 +12,6 @@ Require Import NZAxioms.
 
 Module Type NZBaseProp (Import NZ : NZDomainSig').
 
-(** An artificial scope meant to be substituted later *)
-
-Delimit Scope abstract_scope with abstract.
-Bind Scope abstract_scope with t.
-
 Include BackportEq NZ NZ. (** eq_refl, eq_sym, eq_trans *)
 
 Lemma eq_sym_iff : forall x y, x==y <-> y==x.
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 072b75f78..380963cff 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -28,23 +28,13 @@ Require Import CyclicAxioms Cyclic31 Ring31 NSig NSigNAxioms NMake
 
 Delimit Scope bigN_scope with bigN.
 
-Module BigN <: NType <: OrderedTypeFull <: TotalOrder.
- Include NMake.Make Int31Cyclic [scope abstract_scope to bigN_scope].
- Bind Scope bigN_scope with t t'.
- Include NTypeIsNAxioms
+Module BigN <: NType <: OrderedTypeFull <: TotalOrder :=
+  NMake.Make Int31Cyclic
+  <+ NTypeIsNAxioms
   <+ NProp [no inline]
   <+ HasEqBool2Dec [no inline]
   <+ MinMaxLogicalProperties [no inline]
   <+ MinMaxDecProperties [no inline].
-End BigN.
-
-(** Nota concerning scopes : for the first Include, we cannot bind
-    the scope bigN_scope to a type that doesn't exists yet.
-    We hence need to explicitely declare the scope substitution.
-    For the next Include, the abstract type t (in scope abstract_scope)
-    gets substituted to concrete BigN.t (in scope bigN_scope),
-    and the corresponding argument scope are fixed automatically.
-*)
 
 (** Notations about [BigN] *)
 
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index b941ed48f..b28ce15b9 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -138,8 +138,6 @@ pr
   pr "";
   pr " Definition t := t'.";
   pr "";
-  pr " Bind Scope abstract_scope with t t'.";
-  pr "";
 
   pr " (** * A generic toolbox for building and deconstructing [t] *)";
   pr "";
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index a510b3ae2..5e36916b9 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -800,6 +800,8 @@ Include NProp
 
 End Nat.
 
+Bind Scope nat_scope with Nat.t nat.
+
 (** [Nat] contains an [order] tactic for natural numbers *)
 
 (** Note that [Nat.order] is domain-agnostic: it will not prove
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index a2bc5e266..50c90757a 100644
--- a/theories/Numbers/Rational/BigQ/BigQ.v
+++ b/theories/Numbers/Rational/BigQ/BigQ.v
@@ -38,9 +38,8 @@ End BigN_BigZ.
 Delimit Scope bigQ_scope with bigQ.
 
 Module BigQ <: QType <: OrderedTypeFull <: TotalOrder.
- Include QMake.Make BigN BigZ BigN_BigZ [scope abstract_scope to bigQ_scope].
- Bind Scope bigQ_scope with t t_.
- Include !QProperties <+ HasEqBool2Dec
+ Include QMake.Make BigN BigZ BigN_BigZ
+  <+ !QProperties <+ HasEqBool2Dec
   <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties.
  Ltac order := Private_Tac.order.
 End BigQ.
diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v
index a13bb5114..167be6d70 100644
--- a/theories/Numbers/Rational/BigQ/QMake.v
+++ b/theories/Numbers/Rational/BigQ/QMake.v
@@ -39,8 +39,6 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
 
  Definition t := t_.
 
- Bind Scope abstract_scope with t t_.
-
  (** Specification with respect to [QArith] *)
 
  Local Open Scope Q_scope.
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index be5858718..aa065e3c5 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -1840,6 +1840,8 @@ Qed.
 
 End Pos.
 
+Bind Scope positive_scope with Pos.t positive.
+
 (** Exportation of notations *)
 
 Infix "+" := Pos.add : positive_scope.
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index eeec9042f..6948d420a 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1153,11 +1153,9 @@ 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 := _.
 
-(** The Bind Scope prevents Z to stay associated with abstract_scope.
-    (TODO FIX) *)
-
-Include ZProp. Bind Scope Z_scope with Z.
-Include UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
+Include ZProp
+ <+ UsualMinMaxLogicalProperties
+ <+ UsualMinMaxDecProperties.
 
 (** In generic statements, the predicates [lt] and [le] have been
   favored, whereas [gt] and [ge] don't even exist in the abstract
@@ -1277,6 +1275,8 @@ Qed.
 
 End Z.
 
+Bind Scope Z_scope with Z.t Z.
+
 (** Re-export Notations *)
 
 Infix "+" := Z.add : Z_scope.