aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/NatInt/NZProperties.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers/NatInt/NZProperties.v')
-rw-r--r--theories/Numbers/NatInt/NZProperties.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/NatInt/NZProperties.v b/theories/Numbers/NatInt/NZProperties.v
index 781d06594..125b4f62c 100644
--- a/theories/Numbers/NatInt/NZProperties.v
+++ b/theories/Numbers/NatInt/NZProperties.v
@@ -17,4 +17,4 @@ Require Export NZAxioms NZMulOrder.
subsumes all others.
*)
-Module NZPropFunct := NZMulOrderPropFunct.
+Module Type NZPropFunct := NZMulOrderPropSig.