An automatic substitution of scope at functor application

 For Argument Scope, we now record types (more precisely classes cl_typ)
 in addition to scope list. After substitution (e.g. at functor application),
 the new types are used to search for corresponding concrete scopes.

 Currently, this automatic scope substitution of argument scope takes
 precedence (if successful) over scope declared in the functor (even
 by the user). On the opposite, the manual scope substitution
 (cf last commit introducing annotation [scope foo to bar])
 is done _after_ the automatic scope substitution.

 TODO: if this behavior is satisfactory, document it ...

 Note that Classops.find_class_type lose its env args since it was
 actually unused, and is now used for Notation.find_class

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

5 files changed, 34 insertions, 23 deletions

diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 9748a4366..236c56b9f 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -26,13 +26,17 @@ Require Import ZProperties ZDivFloor ZSig ZSigZAxioms ZMake.
 
 Delimit Scope bigZ_scope with bigZ.
 
-Module BigZ <: ZType <: OrderedTypeFull <: TotalOrder :=
- ZMake.Make BigN [scope abstract_scope to bigZ_scope]
- <+ ZTypeIsZAxioms [scope abstract_scope to bigZ_scope]
- <+ ZProp [no inline, scope abstract_scope to bigZ_scope]
- <+ HasEqBool2Dec [no inline, scope abstract_scope to bigZ_scope]
- <+ MinMaxLogicalProperties [no inline, scope abstract_scope to bigZ_scope]
- <+ MinMaxDecProperties [no inline, scope abstract_scope to bigZ_scope].
+Module BigZ <: ZType <: OrderedTypeFull <: TotalOrder.
+ Include ZMake.Make BigN [scope abstract_scope to bigZ_scope].
+ Bind Scope bigZ_scope with t t_.
+ Include 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 *)
 
 (** Notations about [BigZ] *)
 
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index fbb91ef7f..366418035 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -223,9 +223,8 @@ Definition eq := (@eq Z).
 
 (** Now the generic properties. *)
 
-Include ZProp [scope abstract_scope to Z_scope]
- <+ UsualMinMaxLogicalProperties [scope abstract_scope to Z_scope]
- <+ UsualMinMaxDecProperties [scope abstract_scope to Z_scope].
+Include ZProp
+ <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
 
 End Z.
 
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 858c06658..d2c93bbfd 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -28,13 +28,23 @@ Require Import CyclicAxioms Cyclic31 Ring31 NSig NSigNAxioms NMake
 
 Delimit Scope bigN_scope with bigN.
 
-Module BigN <: NType <: OrderedTypeFull <: TotalOrder :=
- NMake.Make Int31Cyclic [scope abstract_scope to bigN_scope]
- <+ NTypeIsNAxioms [scope abstract_scope to bigN_scope]
- <+ NProp [no inline, scope abstract_scope to bigN_scope]
- <+ HasEqBool2Dec [no inline, scope abstract_scope to bigN_scope]
- <+ MinMaxLogicalProperties [no inline, scope abstract_scope to bigN_scope]
- <+ MinMaxDecProperties [no inline, scope abstract_scope to bigN_scope].
+Module BigN <: NType <: OrderedTypeFull <: TotalOrder.
+ Include NMake.Make Int31Cyclic [scope abstract_scope to bigN_scope].
+ Bind Scope bigN_scope with t t'.
+ Include 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/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index cf284a2f1..bd59ef494 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -234,9 +234,8 @@ Definition lor := Nor.
 Definition ldiff := Ndiff.
 Definition div2 := Ndiv2.
 
-Include NProp [scope abstract_scope to N_scope]
- <+ UsualMinMaxLogicalProperties [scope abstract_scope to N_scope]
- <+ UsualMinMaxDecProperties [scope abstract_scope to N_scope].
+Include NProp
+ <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
 
 End N.
 
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 4578851e2..0cf9ae441 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -756,9 +756,8 @@ Definition div2_spec a : div2 a = shiftr a 1 := eq_refl _.
 
 (** Generic Properties *)
 
-Include NProp [scope abstract_scope to nat_scope]
- <+ UsualMinMaxLogicalProperties [scope abstract_scope to nat_scope]
- <+ UsualMinMaxDecProperties [scope abstract_scope to nat_scope].
+Include NProp
+ <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
 
 End Nat.