diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-13 00:42:57 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-13 00:42:57 +0000 |
| commit | 7cadf058d5f94cbd79f9318d6045e050994091c8 (patch) | |
| tree | 9db84752627c801d3abd99abb6f0da13fa947493 /theories/Numbers/NatInt | |
| parent | 33c0d04c1ae40fb3eded886f8d82eb941e588fc9 (diff) | |
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
Diffstat (limited to 'theories/Numbers/NatInt')
| -rw-r--r-- | theories/Numbers/NatInt/NZOrder.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index 5582438b7..1f23bf37a 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. +*) |