OrderedType implementation for various numerical datatypes + min/max structures

 - A richer OrderedTypeFull interface : OrderedType + predicate "le"
 - Implementations {Nat,N,P,Z,Q}OrderedType.v, also providing "order" tactics
 - By the way: as suggested by S. Lescuyer, specification of compare is
   now inductive
 - GenericMinMax: axiomatisation + properties of min and max out of
    OrderedTypeFull structures.
 - MinMax.v, {Z,P,N,Q}minmax.v are specialization of GenericMinMax,
    with also some domain-specific results, and compatibility layer
    with already existing results.
 - Some ML code of plugins had to be adapted, otherwise wrong "eq",
   "lt" or simimlar constants were found by functions like coq_constant.
 - Beware of the aliasing problems: for instance eq:=@eq t instead of
   eq:=@eq M.t in Make_UDT made (r)omega stopped working (Z_as_OT.t
   instead of Z in statement of Zmax_spec).
 - Some Morphism declaration are now ambiguous: switch to new syntax
   anyway.
 - Misc adaptations of FSets/MSets
 - Classes/RelationPairs.v: from two relations over A and B, we
   inspect relations over A*B and their properties in terms of classes.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12461 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 30 deletions

diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v
index 5b0fb21ef..de7a20d4c 100644
--- a/theories/Structures/DecidableType.v
+++ b/theories/Structures/DecidableType.v
@@ -9,44 +9,19 @@
 (* $Id$ *)
 
 Require Export SetoidList.
+Require DecidableType2. (* No Import here, this is on purpose. *)
+
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-(** * Types with Equalities, and nothing more (for subtyping purpose) *)
-
-Module Type EqualityType.
-
-  Parameter Inline t : Type.
 
-  Parameter Inline eq : t -> t -> Prop.
-
-  Axiom eq_refl : forall x : t, eq x x.
-  Axiom eq_sym : forall x y : t, eq x y -> eq y x.
-  Axiom eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
-
-  Hint Immediate eq_sym.
-  Hint Resolve eq_refl eq_trans.
+(** * Types with Equalities, and nothing more (for subtyping purpose) *)
 
-End EqualityType.
+Module Type EqualityType := DecidableType2.EqualityTypeOrig.
 
 (** * Types with decidable Equalities (but no ordering) *)
 
-Module Type DecidableType.
-
-  Parameter Inline t : Type.
-
-  Parameter Inline eq : t -> t -> Prop.
-
-  Axiom eq_refl : forall x : t, eq x x.
-  Axiom eq_sym : forall x y : t, eq x y -> eq y x.
-  Axiom eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
-
-  Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }.
-
-  Hint Immediate eq_sym.
-  Hint Resolve eq_refl eq_trans.
-
-End DecidableType.
+Module Type DecidableType := DecidableType2.DecidableTypeOrig.
 
 (** * Additional notions about keys and datas used in FMap *)