diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-02-11 16:54:20 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-02-11 16:54:20 +0000 |
| commit | 889c0bbb3762f3c85663273e58a46815a9d1f8f5 (patch) | |
| tree | 3e13c101710bfb202b4f1229e23e955eafbc7311 /theories/Numbers/Integer | |
| parent | 483e36a76c4a31a1711a4602be45f66e7f46760f (diff) | |
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
Diffstat (limited to 'theories/Numbers/Integer')
| -rw-r--r-- | theories/Numbers/Integer/BigZ/BigZ.v | 18 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Binary/ZBinary.v | 5 |
2 files changed, 13 insertions, 10 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. |