diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-07-17 15:31:36 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-07-17 15:31:36 +0000 |
commit | 3d09e39dd423d81c6af3e991d5b282ea8608646b (patch) | |
tree | ae5e89db801b216b6152fb7d6bd0d7efe855ef57 /theories/Numbers/Natural | |
parent | 9f3fc5d04b69f0c6bf6eec56c32ed11a218dde61 (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/Natural')
-rw-r--r-- | theories/Numbers/Natural/BigN/BigN.v | 16 | ||||
-rw-r--r-- | theories/Numbers/Natural/BigN/NMake_gen.ml | 2 | ||||
-rw-r--r-- | theories/Numbers/Natural/Peano/NPeano.v | 2 |
3 files changed, 5 insertions, 15 deletions
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index 072b75f78..380963cff 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -28,23 +28,13 @@ Require Import CyclicAxioms Cyclic31 Ring31 NSig NSigNAxioms NMake Delimit Scope bigN_scope with bigN. -Module BigN <: NType <: OrderedTypeFull <: TotalOrder. - Include NMake.Make Int31Cyclic [scope abstract_scope to bigN_scope]. - Bind Scope bigN_scope with t t'. - Include NTypeIsNAxioms +Module BigN <: NType <: OrderedTypeFull <: TotalOrder := + NMake.Make Int31Cyclic + <+ 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/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index b941ed48f..b28ce15b9 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -138,8 +138,6 @@ pr pr ""; pr " Definition t := t'."; pr ""; - pr " Bind Scope abstract_scope with t t'."; - pr ""; pr " (** * A generic toolbox for building and deconstructing [t] *)"; pr ""; diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index a510b3ae2..5e36916b9 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -800,6 +800,8 @@ Include NProp End Nat. +Bind Scope nat_scope with Nat.t nat. + (** [Nat] contains an [order] tactic for natural numbers *) (** Note that [Nat.order] is domain-agnostic: it will not prove |