aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/Natural/Abstract
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers/Natural/Abstract')
-rw-r--r--theories/Numbers/Natural/Abstract/NAxioms.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index 09438628d..45a2cf3e1 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -32,11 +32,11 @@ End NDivSpecific.
(** We now group everything together. *)
-Module Type NAxiomsSig := NAxiomsMiniSig <+ HasCompare <+ HasEqBool
+Module Type NAxiomsSig := NAxiomsMiniSig <+ OrderFunctions
<+ NZParity.NZParity <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2
<+ NZGcd.NZGcd <+ NZDiv.NZDiv <+ NZBits.NZBits.
-Module Type NAxiomsSig' := NAxiomsMiniSig' <+ HasCompare <+ HasEqBool
+Module Type NAxiomsSig' := NAxiomsMiniSig' <+ OrderFunctions'
<+ NZParity.NZParity <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2
<+ NZGcd.NZGcd' <+ NZDiv.NZDiv' <+ NZBits.NZBits'.