diff options
Diffstat (limited to 'theories/Numbers/Integer/Axioms/ZTimesOrder.v')
| -rw-r--r-- | theories/Numbers/Integer/Axioms/ZTimesOrder.v | 11 |
1 files changed, 4 insertions, 7 deletions
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. |