diff options
Diffstat (limited to 'theories/Numbers/Integer/Axioms')
-rw-r--r-- | theories/Numbers/Integer/Axioms/ZAxioms.v | 4 | ||||
-rw-r--r-- | theories/Numbers/Integer/Axioms/ZDomain.v | 2 | ||||
-rw-r--r-- | theories/Numbers/Integer/Axioms/ZOrder.v | 4 | ||||
-rw-r--r-- | theories/Numbers/Integer/Axioms/ZPlus.v | 4 | ||||
-rw-r--r-- | theories/Numbers/Integer/Axioms/ZPlusOrder.v | 8 | ||||
-rw-r--r-- | theories/Numbers/Integer/Axioms/ZTimes.v | 5 | ||||
-rw-r--r-- | theories/Numbers/Integer/Axioms/ZTimesOrder.v | 11 |
7 files changed, 13 insertions, 25 deletions
diff --git a/theories/Numbers/Integer/Axioms/ZAxioms.v b/theories/Numbers/Integer/Axioms/ZAxioms.v index b73410256..05b8ede94 100644 --- a/theories/Numbers/Integer/Axioms/ZAxioms.v +++ b/theories/Numbers/Integer/Axioms/ZAxioms.v @@ -1,5 +1,4 @@ -Require Import NumPrelude. -Require Import ZDomain. +Require Export ZDomain. Module Type IntSignature. Declare Module Export DomainModule : DomainSignature. @@ -25,7 +24,6 @@ Axiom induction : End IntSignature. - Module IntProperties (Export IntModule : IntSignature). Module Export DomainPropertiesModule := DomainProperties DomainModule. Open Local Scope ZScope. diff --git a/theories/Numbers/Integer/Axioms/ZDomain.v b/theories/Numbers/Integer/Axioms/ZDomain.v index b48684ba8..1a29eddf2 100644 --- a/theories/Numbers/Integer/Axioms/ZDomain.v +++ b/theories/Numbers/Integer/Axioms/ZDomain.v @@ -1,4 +1,4 @@ -Require Import NumPrelude. +Require Export NumPrelude. Module Type DomainSignature. diff --git a/theories/Numbers/Integer/Axioms/ZOrder.v b/theories/Numbers/Integer/Axioms/ZOrder.v index 3bf4d61f5..803bfe43b 100644 --- a/theories/Numbers/Integer/Axioms/ZOrder.v +++ b/theories/Numbers/Integer/Axioms/ZOrder.v @@ -1,6 +1,4 @@ -Require Import NumPrelude. -Require Import ZDomain. -Require Import ZAxioms. +Require Export ZAxioms. Module Type OrderSignature. Declare Module Export IntModule : IntSignature. diff --git a/theories/Numbers/Integer/Axioms/ZPlus.v b/theories/Numbers/Integer/Axioms/ZPlus.v index f455400b7..484607094 100644 --- a/theories/Numbers/Integer/Axioms/ZPlus.v +++ b/theories/Numbers/Integer/Axioms/ZPlus.v @@ -1,6 +1,4 @@ -Require Import NumPrelude. -Require Import ZDomain. -Require Import ZAxioms. +Require Export ZAxioms. Module Type PlusSignature. Declare Module Export IntModule : IntSignature. diff --git a/theories/Numbers/Integer/Axioms/ZPlusOrder.v b/theories/Numbers/Integer/Axioms/ZPlusOrder.v index 4f677355b..dd311b49a 100644 --- a/theories/Numbers/Integer/Axioms/ZPlusOrder.v +++ b/theories/Numbers/Integer/Axioms/ZPlusOrder.v @@ -1,8 +1,8 @@ -Require Import ZOrder. -Require Import ZPlus. +Require Export ZOrder. +Require Export ZPlus. -Module PlusOrderProperties (Export PlusModule : PlusSignature) - (Export OrderModule : OrderSignature with +Module PlusOrderProperties (PlusModule : PlusSignature) + (OrderModule : OrderSignature with Module IntModule := PlusModule.IntModule). (* Warning: Notation _ == _ was already used in scope ZScope !!! *) Module Export PlusPropertiesModule := PlusProperties PlusModule. diff --git a/theories/Numbers/Integer/Axioms/ZTimes.v b/theories/Numbers/Integer/Axioms/ZTimes.v index ff0de6196..052dcf66f 100644 --- a/theories/Numbers/Integer/Axioms/ZTimes.v +++ b/theories/Numbers/Integer/Axioms/ZTimes.v @@ -1,7 +1,4 @@ -Require Import NumPrelude. -Require Import ZDomain. -Require Import ZAxioms. -Require Import ZPlus. +Require Export ZPlus. Module Type TimesSignature. Declare Module Export PlusModule : PlusSignature. diff --git a/theories/Numbers/Integer/Axioms/ZTimesOrder.v b/theories/Numbers/Integer/Axioms/ZTimesOrder.v index 460a13bf4..a72636a42 100644 --- a/theories/Numbers/Integer/Axioms/ZTimesOrder.v +++ b/theories/Numbers/Integer/Axioms/ZTimesOrder.v @@ -1,12 +1,9 @@ -Require Import ZPlus. -Require Import ZTimes. -Require Import ZOrder. -Require Import ZPlusOrder. +Require Export ZTimes. +Require Export ZPlusOrder. -Module TimesOrderProperties (Export TimesModule : TimesSignature) - (Export OrderModule : OrderSignature with +Module TimesOrderProperties (TimesModule : TimesSignature) + (OrderModule : OrderSignature with Module IntModule := TimesModule.PlusModule.IntModule). - Module Export TimesPropertiesModule := TimesProperties TimesModule. Module Export PlusOrderPropertiesModule := PlusOrderProperties TimesModule.PlusModule OrderModule. |