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

2 files changed, 2 insertions, 5 deletions

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.