aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/Integer
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-07-17 15:31:36 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-07-17 15:31:36 +0000
commit3d09e39dd423d81c6af3e991d5b282ea8608646b (patch)
treeae5e89db801b216b6152fb7d6bd0d7efe855ef57 /theories/Numbers/Integer
parent9f3fc5d04b69f0c6bf6eec56c32ed11a218dde61 (diff)
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
Diffstat (limited to 'theories/Numbers/Integer')
-rw-r--r--theories/Numbers/Integer/BigZ/BigZ.v8
-rw-r--r--theories/Numbers/Integer/BigZ/ZMake.v2
2 files changed, 3 insertions, 7 deletions
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.