diff options
| author |  emakarov <emakarov@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-07-13 17:52:22 +0000 |
|---|---|---|
| committer | emakarov <emakarov@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-07-13 17:52:22 +0000 |
| commit | e8f786b4ef55aae4fc40c46f1b73c185ee0e5819 (patch) | |
| tree | 6c6f65c85a1476572ebca39c975e59c38d2e10d3 /theories/Numbers/Integer/Axioms/ZAxioms.v | |
| parent | 72cd18d711b3e9ea2ecb0d657187dc5febfbc8e3 (diff) | |
An update on axiomatization of number classes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10002 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Integer/Axioms/ZAxioms.v')
| -rw-r--r-- | theories/Numbers/Integer/Axioms/ZAxioms.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/theories/Numbers/Integer/Axioms/ZAxioms.v b/theories/Numbers/Integer/Axioms/ZAxioms.v index 05b8ede94..6527bd11c 100644 --- a/theories/Numbers/Integer/Axioms/ZAxioms.v +++ b/theories/Numbers/Integer/Axioms/ZAxioms.v @@ -1,14 +1,14 @@ Require Export ZDomain. Module Type IntSignature. -Declare Module Export DomainModule : DomainSignature. -Open Local Scope ZScope. +Declare Module Export ZDomainModule : ZDomainSignature. +Open Local Scope IntScope. Parameter Inline O : Z. Parameter Inline S : Z -> Z. Parameter Inline P : Z -> Z. -Notation "0" := O : ZScope. +Notation "0" := O : IntScope. Add Morphism S with signature E ==> E as S_wd. Add Morphism P with signature E ==> E as P_wd. @@ -24,9 +24,9 @@ Axiom induction : End IntSignature. -Module IntProperties (Export IntModule : IntSignature). -Module Export DomainPropertiesModule := DomainProperties DomainModule. -Open Local Scope ZScope. +Module IntProperties (Import IntModule : IntSignature). +Module Export ZDomainPropertiesModule := ZDomainProperties ZDomainModule. +Open Local Scope IntScope. Ltac induct n := try intros until n; |