summaryrefslogtreecommitdiff
path: root/theories/Numbers
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2013-05-08 17:47:16 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2013-05-08 17:47:16 +0200
commit813d651c75cb954677a483b60d880600b421e011 (patch)
treef917021e7e7083cf1ce84f9a560179603f0c7af6 /theories/Numbers
parent0c6687c12b628881d5660d57707f0e7ca9e521b7 (diff)
parent499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff)
Merge tag 'upstream/8.4pl2dfsg' into experimental/master
Upstream version 8.4pl2dfsg
Diffstat (limited to 'theories/Numbers')
-rw-r--r--theories/Numbers/NatInt/NZOrder.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 5582438b..3dae9c70 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -646,4 +646,4 @@ End NZOrderProp.
Module NZOrderedType (NZ : NZDecOrdSig')
<: DecidableTypeFull <: OrderedTypeFull
- := NZ <+ NZBaseProp <+ NZOrderProp <+ Compare2EqBool <+ HasEqBool2Dec.
+ := NZ <+ NZBaseProp <+ NZOrderProp NZ <+ Compare2EqBool <+ HasEqBool2Dec.