From 7cadf058d5f94cbd79f9318d6045e050994091c8 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 13 Feb 2013 00:42:57 +0000
Subject: make validate repaired via a temporary fix for #2949

 The offending functor in NZOrder wasn't actually used, so
 I've commented it for now.

 Btw, the Not_found in coqchk is now turned into something slightly
 more informative

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16199 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/NatInt/NZOrder.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'theories/Numbers')

diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 5582438b7b..1f23bf37a3 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -644,6 +644,8 @@ End NZOrderProp.
 (** If we have moreover a [compare] function, we can build
     an [OrderedType] structure. *)
 
+(* Temporary workaround for bug #2949: remove this problematic + unused functor
 Module NZOrderedType (NZ : NZDecOrdSig')
  <: DecidableTypeFull <: OrderedTypeFull
  := NZ <+ NZBaseProp <+ NZOrderProp <+ Compare2EqBool <+ HasEqBool2Dec.
+*)
-- 
cgit v1.2.3