Rework of GenericMinMax and OrdersTac (helps extraction, cf. #2904)

 Inner sub-modules with "Definition t := t" is hard to handle by
 extraction: "type t = t" is recursive by default in OCaml, and
 the aliased t cannot easily be fully qualified if it comes from
 a higher unterminated module. There already exists some workarounds
 (generating Coq__XXX modules), but this isn't playing nicely with
 module types, where it's hard to insert code without breaking
 subtyping.

 To avoid falling too often in this situation, I've reorganized:

 - GenericMinMax : we do not try anymore to deduce facts about
   min by saying "min is a max on the reversed order". This hack
   was anyway not so nice, some code was duplicated nonetheless
   (at least statements), and the module structure was complex.

 - OrdersTac : by splitting the functor argument in two
   (EqLtLe <+ IsTotalOrder instead of TotalOrder), we avoid
   the need for aliasing the type t, cf NZOrder.

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

1 files changed, 15 insertions, 13 deletions

diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index beb10a833..fa08f9366 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -108,19 +108,21 @@ Module OrderedTypeFacts (Import O: OrderedType).
   Lemma lt_total : forall x y, lt x y \/ eq x y \/ lt y x.
   Proof. intros; destruct (compare x y); auto. Qed.
 
-  Module OrderElts <: Orders.TotalOrder.
-  Definition t := t.
-  Definition eq := eq.
-  Definition lt := lt.
-  Definition le x y := lt x y \/ eq x y.
-  Definition eq_equiv := eq_equiv.
-  Definition lt_strorder := lt_strorder.
-  Definition lt_compat := lt_compat.
-  Definition lt_total := lt_total.
-  Lemma le_lteq : forall x y, le x y <-> lt x y \/ eq x y.
-  Proof. unfold le; intuition. Qed.
-  End OrderElts.
-  Module OrderTac := !MakeOrderTac OrderElts.
+  Module TO.
+   Definition t := t.
+   Definition eq := eq.
+   Definition lt := lt.
+   Definition le x y := lt x y \/ eq x y.
+  End TO.
+  Module IsTO.
+   Definition eq_equiv := eq_equiv.
+   Definition lt_strorder := lt_strorder.
+   Definition lt_compat := lt_compat.
+   Definition lt_total := lt_total.
+   Lemma le_lteq x y : TO.le x y <-> lt x y \/ eq x y.
+   Proof. reflexivity. Qed.
+  End IsTO.
+  Module OrderTac := !MakeOrderTac TO IsTO.
   Ltac order := OrderTac.order.
 
   Lemma le_eq x y z : ~lt x y -> eq y z -> ~lt x z. Proof. order. Qed.