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

1 files changed, 17 insertions, 7 deletions

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] *)