diff options
Diffstat (limited to 'theories/Numbers/NatInt/NZAxioms.v')
| -rw-r--r-- | theories/Numbers/NatInt/NZAxioms.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v index 5b4e16cafe..480314f96f 100644 --- a/theories/Numbers/NatInt/NZAxioms.v +++ b/theories/Numbers/NatInt/NZAxioms.v @@ -10,7 +10,7 @@ (*i $Id$ i*) -Require Export DecidableType2 OrderedType2 NumPrelude GenericMinMax. +Require Export Equalities Orders NumPrelude GenericMinMax. (** Axiomatization of a domain with zero, successor, predecessor, and a bi-directional induction principle. We require [P (S n) = n] |