diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-02-11 16:54:18 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-02-11 16:54:18 +0000 |
| commit | 483e36a76c4a31a1711a4602be45f66e7f46760f (patch) | |
| tree | 6a490563e2a55d14e91da600f3843b8fc0b09552 /theories/Numbers/NatInt | |
| parent | 1e1bc1952499bf3528810f2b3e6efad76ab843d0 (diff) | |
Annotations at functor applications:
- The experimental syntax "<30>F M" is transformed into "F M [inline at level 30]"
- The earlier syntax !F X should now be written "F X [no inline]"
(note that using ! is still possible for compatibility)
- A new annotation "F M [scope foo_scope to bar_scope]" allow to substitute
foo_scope by bar_scope in all arguments scope of objects in F.
BigN and BigZ are cleaned from the zillions of Arguments Scope used earlier.
Arguments scope for lemmas are fixed for instances of Numbers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13839 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/NatInt')
| -rw-r--r-- | theories/Numbers/NatInt/NZBase.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v index 56fad9347..65b646356 100644 --- a/theories/Numbers/NatInt/NZBase.v +++ b/theories/Numbers/NatInt/NZBase.v @@ -12,6 +12,11 @@ Require Import NZAxioms. Module Type NZBaseProp (Import NZ : NZDomainSig'). +(** An artificial scope meant to be substituted later *) + +Delimit Scope abstract_scope with abstract. +Bind Scope abstract_scope with t. + Include BackportEq NZ NZ. (** eq_refl, eq_sym, eq_trans *) Lemma eq_sym_iff : forall x y, x==y <-> y==x. |