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