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

3 files changed, 245 insertions, 269 deletions

diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v
index 5583142f8..ffd0649af 100644
--- a/theories/Structures/GenericMinMax.v
+++ b/theories/Structures/GenericMinMax.v
@@ -40,34 +40,34 @@ Module GenericMinMax (Import O:OrderedTypeFull') <: HasMinMax O.
  Definition max := gmax O.compare.
  Definition min := gmin O.compare.
 
- Lemma ge_not_lt : forall x y, y<=x -> x<y -> False.
+ Lemma ge_not_lt x y : y<=x -> x<y -> False.
  Proof.
- intros x y H H'.
+ intros H H'.
  apply (StrictOrder_Irreflexive x).
  rewrite le_lteq in *; destruct H as [H|H].
  transitivity y; auto.
  rewrite H in H'; auto.
  Qed.
 
- Lemma max_l : forall x y, y<=x -> max x y == x.
+ Lemma max_l x y : y<=x -> max x y == x.
  Proof.
  intros. unfold max, gmax. case compare_spec; auto with relations.
  intros; elim (ge_not_lt x y); auto.
  Qed.
 
- Lemma max_r : forall x y, x<=y -> max x y == y.
+ Lemma max_r x y : x<=y -> max x y == y.
  Proof.
  intros. unfold max, gmax. case compare_spec; auto with relations.
  intros; elim (ge_not_lt y x); auto.
  Qed.
 
- Lemma min_l : forall x y, x<=y -> min x y == x.
+ Lemma min_l x y : x<=y -> min x y == x.
  Proof.
  intros. unfold min, gmin. case compare_spec; auto with relations.
  intros; elim (ge_not_lt y x); auto.
  Qed.
 
- Lemma min_r : forall x y, y<=x -> min x y == y.
+ Lemma min_r x y : y<=x -> min x y == y.
  Proof.
  intros. unfold min, gmin. case compare_spec; auto with relations.
  intros; elim (ge_not_lt x y); auto.
@@ -76,31 +76,30 @@ Module GenericMinMax (Import O:OrderedTypeFull') <: HasMinMax O.
 End GenericMinMax.
 
 
-(** ** Consequences of the minimalist interface: facts about [max]. *)
+(** ** Consequences of the minimalist interface: facts about [max] and [min]. *)
 
-Module MaxLogicalProperties (Import O:TotalOrder')(Import M:HasMax O).
- Module Import Private_Tac := !MakeOrderTac O.
+Module MinMaxLogicalProperties (Import O:TotalOrder')(Import M:HasMinMax O).
+ Module Import Private_Tac := !MakeOrderTac O O.
 
 (** An alternative caracterisation of [max], equivalent to
     [max_l /\ max_r] *)
 
-Lemma max_spec : forall n m,
-  (n < m /\ max n m == m)  \/ (m <= n /\ max n m == n).
+Lemma max_spec n m :
+  (n < m /\ max n m == m) \/ (m <= n /\ max n m == n).
 Proof.
- intros n m.
  destruct (lt_total n m); [left|right].
- split; auto. apply max_r. rewrite le_lteq; auto.
- assert (m <= n) by (rewrite le_lteq; intuition).
- split; auto. apply max_l; auto.
+ - split; auto. apply max_r. rewrite le_lteq; auto.
+ - assert (m <= n) by (rewrite le_lteq; intuition).
+   split; auto. now apply max_l.
 Qed.
 
 (** A more symmetric version of [max_spec], based only on [le].
     Beware that left and right alternatives overlap. *)
 
-Lemma max_spec_le : forall n m,
+Lemma max_spec_le n m :
  (n <= m /\ max n m == m) \/ (m <= n /\ max n m == n).
 Proof.
- intros. destruct (max_spec n m); [left|right]; intuition; order.
+ destruct (max_spec n m); [left|right]; intuition; order.
 Qed.
 
 Instance : Proper (eq==>eq==>iff) le.
@@ -108,25 +107,24 @@ Proof. repeat red. intuition order. Qed.
 
 Instance max_compat : Proper (eq==>eq==>eq) max.
 Proof.
-intros x x' Hx y y' Hy.
-assert (H1 := max_spec x y). assert (H2 := max_spec x' y').
-set (m := max x y) in *; set (m' := max x' y') in *; clearbody m m'.
-rewrite <- Hx, <- Hy in *.
-destruct (lt_total x y); intuition order.
+ intros x x' Hx y y' Hy.
+ assert (H1 := max_spec x y). assert (H2 := max_spec x' y').
+ set (m := max x y) in *; set (m' := max x' y') in *; clearbody m m'.
+ rewrite <- Hx, <- Hy in *.
+ destruct (lt_total x y); intuition order.
 Qed.
 
-
 (** A function satisfying the same specification is equal to [max]. *)
 
-Lemma max_unicity : forall n m p,
- ((n < m /\ p == m)  \/ (m <= n /\ p == n)) ->  p == max n m.
+Lemma max_unicity n m p :
+ ((n < m /\ p == m) \/ (m <= n /\ p == n)) -> p == max n m.
 Proof.
- intros. assert (Hm := max_spec n m).
+ assert (Hm := max_spec n m).
  destruct (lt_total n m); intuition; order.
 Qed.
 
-Lemma max_unicity_ext : forall f,
- (forall n m, (n < m /\ f n m == m)  \/ (m <= n /\ f n m == n)) ->
+Lemma max_unicity_ext f :
+ (forall n m, (n < m /\ f n m == m) \/ (m <= n /\ f n m == n)) ->
  (forall n m, f n m == max n m).
 Proof.
  intros. apply max_unicity; auto.
@@ -134,12 +132,12 @@ Qed.
 
 (** [max] commutes with monotone functions. *)
 
-Lemma max_mono: forall f,
+Lemma max_mono f :
  (Proper (eq ==> eq) f) ->
  (Proper (le ==> le) f) ->
  forall x y, max (f x) (f y) == f (max x y).
 Proof.
- intros f Eqf Lef x y.
+ intros Eqf Lef x y.
  destruct (max_spec x y) as [(H,E)|(H,E)]; rewrite E;
   destruct (max_spec (f x) (f y)) as [(H',E')|(H',E')]; auto.
  assert (f x <= f y) by (apply Lef; order). order.
@@ -148,239 +146,232 @@ Qed.
 
 (** *** Semi-lattice algebraic properties of [max] *)
 
-Lemma max_id : forall n, max n n == n.
+Lemma max_id n : max n n == n.
 Proof.
- intros. destruct (max_spec n n); intuition.
+ apply max_l; order.
 Qed.
 
 Notation max_idempotent := max_id (only parsing).
 
-Lemma max_assoc : forall m n p, max m (max n p) == max (max m n) p.
+Lemma max_assoc m n p : max m (max n p) == max (max m n) p.
 Proof.
- intros.
- destruct (max_spec n p) as [(H,Eq)|(H,Eq)]; rewrite Eq.
- destruct (max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'.
- destruct (max_spec m p); intuition; order. order.
- destruct (max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'. order.
- destruct (max_spec m p); intuition; order.
+ destruct (max_spec n p) as [(H,E)|(H,E)]; rewrite E;
+ destruct (max_spec m n) as [(H',E')|(H',E')]; rewrite E', ?E; try easy.
+ - apply max_r; order.
+ - symmetry. apply max_l; order.
 Qed.
 
-Lemma max_comm : forall n m, max n m == max m n.
+Lemma max_comm n m : max n m == max m n.
 Proof.
- intros.
- destruct (max_spec n m) as [(H,Eq)|(H,Eq)]; rewrite Eq.
- destruct (max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; order.
- destruct (max_spec m n) as [(H',Eq')|(H',Eq')]; rewrite Eq'; order.
+ destruct (max_spec m n) as [(H,E)|(H,E)]; rewrite E;
+  (apply max_r || apply max_l); order.
 Qed.
 
+Ltac solve_max :=
+ match goal with |- context [max ?n ?m] =>
+  destruct (max_spec n m); intuition; order
+ end.
+
 (** *** Least-upper bound properties of [max] *)
 
-Lemma le_max_l : forall n m, n <= max n m.
-Proof.
- intros; destruct (max_spec n m); intuition; order.
-Qed.
+Lemma le_max_l n m : n <= max n m.
+Proof. solve_max. Qed.
 
-Lemma le_max_r : forall n m, m <= max n m.
-Proof.
- intros; destruct (max_spec n m); intuition; order.
-Qed.
+Lemma le_max_r n m : m <= max n m.
+Proof. solve_max. Qed.
 
-Lemma max_l_iff : forall n m, max n m == n <-> m <= n.
-Proof.
- split. intro H; rewrite <- H. apply le_max_r. apply max_l.
-Qed.
+Lemma max_l_iff n m : max n m == n <-> m <= n.
+Proof. solve_max. Qed.
 
-Lemma max_r_iff : forall n m, max n m == m <-> n <= m.
-Proof.
- split. intro H; rewrite <- H. apply le_max_l. apply max_r.
-Qed.
+Lemma max_r_iff n m : max n m == m <-> n <= m.
+Proof. solve_max. Qed.
 
-Lemma max_le : forall n m p, p <= max n m -> p <= n \/ p <= m.
+Lemma max_le n m p : p <= max n m -> p <= n \/ p <= m.
 Proof.
- intros n m p H; destruct (max_spec n m);
-  [right|left]; intuition; order.
+ destruct (max_spec n m); [right|left]; intuition; order.
 Qed.
 
-Lemma max_le_iff : forall n m p, p <= max n m <-> p <= n \/ p <= m.
-Proof.
- intros. split. apply max_le.
- destruct (max_spec n m); intuition; order.
-Qed.
+Lemma max_le_iff n m p : p <= max n m <-> p <= n \/ p <= m.
+Proof. split. apply max_le. solve_max. Qed.
 
-Lemma max_lt_iff : forall n m p, p < max n m <-> p < n \/ p < m.
+Lemma max_lt_iff n m p : p < max n m <-> p < n \/ p < m.
 Proof.
- intros. destruct (max_spec n m); intuition;
+ destruct (max_spec n m); intuition;
   order || (right; order) || (left; order).
 Qed.
 
-Lemma max_lub_l : forall n m p, max n m <= p -> n <= p.
-Proof.
- intros; destruct (max_spec n m); intuition; order.
-Qed.
+Lemma max_lub_l n m p : max n m <= p -> n <= p.
+Proof. solve_max. Qed.
 
-Lemma max_lub_r : forall n m p, max n m <= p -> m <= p.
-Proof.
- intros; destruct (max_spec n m); intuition; order.
-Qed.
+Lemma max_lub_r n m p : max n m <= p -> m <= p.
+Proof. solve_max. Qed.
 
-Lemma max_lub : forall n m p, n <= p -> m <= p -> max n m <= p.
-Proof.
- intros; destruct (max_spec n m); intuition; order.
-Qed.
+Lemma max_lub n m p : n <= p -> m <= p -> max n m <= p.
+Proof. solve_max. Qed.
 
-Lemma max_lub_iff : forall n m p, max n m <= p <-> n <= p /\ m <= p.
-Proof.
- intros; destruct (max_spec n m); intuition; order.
-Qed.
+Lemma max_lub_iff n m p : max n m <= p <-> n <= p /\ m <= p.
+Proof. solve_max. Qed.
 
-Lemma max_lub_lt : forall n m p, n < p -> m < p -> max n m < p.
-Proof.
- intros; destruct (max_spec n m); intuition; order.
-Qed.
+Lemma max_lub_lt n m p : n < p -> m < p -> max n m < p.
+Proof. solve_max. Qed.
 
-Lemma max_lub_lt_iff : forall n m p, max n m < p <-> n < p /\ m < p.
-Proof.
- intros; destruct (max_spec n m); intuition; order.
-Qed.
+Lemma max_lub_lt_iff n m p : max n m < p <-> n < p /\ m < p.
+Proof. solve_max. Qed.
 
-Lemma max_le_compat_l : forall n m p, n <= m -> max p n <= max p m.
-Proof.
- intros.
- destruct (max_spec p n) as [(LT,E)|(LE,E)]; rewrite E.
- assert (LE' := le_max_r p m). order.
- apply le_max_l.
-Qed.
+Lemma max_le_compat_l n m p : n <= m -> max p n <= max p m.
+Proof. intros. apply max_lub_iff. solve_max. Qed.
 
-Lemma max_le_compat_r : forall n m p, n <= m -> max n p <= max m p.
-Proof.
- intros. rewrite (max_comm n p), (max_comm m p).
- auto using max_le_compat_l.
-Qed.
+Lemma max_le_compat_r n m p : n <= m -> max n p <= max m p.
+Proof. intros. apply max_lub_iff. solve_max. Qed.
 
-Lemma max_le_compat : forall n m p q, n <= m -> p <= q ->
- max n p <= max m q.
+Lemma max_le_compat n m p q : n <= m -> p <= q -> max n p <= max m q.
 Proof.
- intros  n m p q Hnm Hpq.
+ intros Hnm Hpq.
  assert (LE := max_le_compat_l _ _ m Hpq).
  assert (LE' := max_le_compat_r _ _ p Hnm).
  order.
 Qed.
 
-End MaxLogicalProperties.
-
-
-(** ** Properties concernant [min], then both [min] and [max].
+(** Properties of [min] *)
 
-   To avoid too much code duplication, we exploit that [min] can be
-   seen as a [max] of the reversed order.
-*)
+Lemma min_spec n m :
+ (n < m /\ min n m == n) \/ (m <= n /\ min n m == m).
+Proof.
+ destruct (lt_total n m); [left|right].
+ - split; auto. apply min_l. rewrite le_lteq; auto.
+ - assert (m <= n) by (rewrite le_lteq; intuition).
+   split; auto. now apply min_r.
+Qed.
 
-Module MinMaxLogicalProperties (Import O:TotalOrder')(Import M:HasMinMax O).
- Include MaxLogicalProperties O M.
- Import Private_Tac.
-
- Module Import Private_Rev.
- Module ORev := TotalOrderRev O.
- Module MRev <: HasMax ORev.
-  Definition max x y := M.min y x.
-  Definition max_l x y := M.min_r y x.
-  Definition max_r x y := M.min_l y x.
- End MRev.
- Module MPRev := MaxLogicalProperties ORev MRev.
- End Private_Rev.
+Lemma min_spec_le n m :
+ (n <= m /\ min n m == n) \/ (m <= n /\ min n m == m).
+Proof.
+ destruct (min_spec n m); [left|right]; intuition; order.
+Qed.
 
 Instance min_compat : Proper (eq==>eq==>eq) min.
-Proof. intros x x' Hx y y' Hy. apply MPRev.max_compat; assumption. Qed.
+Proof.
+intros x x' Hx y y' Hy.
+assert (H1 := min_spec x y). assert (H2 := min_spec x' y').
+set (m := min x y) in *; set (m' := min x' y') in *; clearbody m m'.
+rewrite <- Hx, <- Hy in *.
+destruct (lt_total x y); intuition order.
+Qed.
 
-Lemma min_spec : forall n m,
- (n < m /\ min n m == n) \/ (m <= n /\ min n m == m).
-Proof. intros. exact (MPRev.max_spec m n). Qed.
+Lemma min_unicity n m p :
+ ((n < m /\ p == n) \/ (m <= n /\ p == m)) ->  p == min n m.
+Proof.
+ assert (Hm := min_spec n m).
+ destruct (lt_total n m); intuition; order.
+Qed.
 
-Lemma min_spec_le : forall n m,
- (n <= m /\ min n m == n) \/ (m <= n /\ min n m == m).
-Proof. intros. exact (MPRev.max_spec_le m n). Qed.
+Lemma min_unicity_ext f :
+ (forall n m, (n < m /\ f n m == n)  \/ (m <= n /\ f n m == m)) ->
+ (forall n m, f n m == min n m).
+Proof.
+ intros. apply min_unicity; auto.
+Qed.
 
-Lemma min_mono: forall f,
+Lemma min_mono f :
  (Proper (eq ==> eq) f) ->
  (Proper (le ==> le) f) ->
  forall x y, min (f x) (f y) == f (min x y).
 Proof.
- intros. apply MPRev.max_mono; auto. compute in *; eauto.
+ intros Eqf Lef x y.
+ destruct (min_spec x y) as [(H,E)|(H,E)]; rewrite E;
+  destruct (min_spec (f x) (f y)) as [(H',E')|(H',E')]; auto.
+ assert (f x <= f y) by (apply Lef; order). order.
+ assert (f y <= f x) by (apply Lef; order). order.
 Qed.
 
-Lemma min_unicity : forall n m p,
- ((n < m /\ p == n)  \/ (m <= n /\ p == m)) ->  p == min n m.
-Proof. intros n m p. apply MPRev.max_unicity. Qed.
-
-Lemma min_unicity_ext : forall f,
- (forall n m, (n < m /\ f n m == n)  \/ (m <= n /\ f n m == m)) ->
- (forall n m, f n m == min n m).
-Proof. intros f H n m. apply MPRev.max_unicity, H; auto. Qed.
-
-Lemma min_id : forall n, min n n == n.
-Proof. intros. exact (MPRev.max_id n). Qed.
+Lemma min_id n : min n n == n.
+Proof.
+ apply min_l; order.
+Qed.
 
 Notation min_idempotent := min_id (only parsing).
 
-Lemma min_assoc : forall m n p, min m (min n p) == min (min m n) p.
-Proof. intros. symmetry; apply MPRev.max_assoc. Qed.
+Lemma min_assoc m n p : min m (min n p) == min (min m n) p.
+Proof.
+ destruct (min_spec n p) as [(H,E)|(H,E)]; rewrite E;
+ destruct (min_spec m n) as [(H',E')|(H',E')]; rewrite E', ?E; try easy.
+ - symmetry. apply min_l; order.
+ - apply min_r; order.
+Qed.
 
-Lemma min_comm : forall n m, min n m == min m n.
-Proof. intros. exact (MPRev.max_comm m n). Qed.
+Lemma min_comm n m : min n m == min m n.
+Proof.
+ destruct (min_spec m n) as [(H,E)|(H,E)]; rewrite E;
+  (apply min_r || apply min_l); order.
+Qed.
 
-Lemma le_min_r : forall n m, min n m <= m.
-Proof. intros. exact (MPRev.le_max_l m n). Qed.
+Ltac solve_min :=
+ match goal with |- context [min ?n ?m] =>
+  destruct (min_spec n m); intuition; order
+ end.
 
-Lemma le_min_l : forall n m, min n m <= n.
-Proof. intros. exact (MPRev.le_max_r m n). Qed.
+Lemma le_min_r n m : min n m <= m.
+Proof. solve_min. Qed.
 
-Lemma min_l_iff : forall n m, min n m == n <-> n <= m.
-Proof. intros n m. exact (MPRev.max_r_iff m n). Qed.
+Lemma le_min_l n m : min n m <= n.
+Proof. solve_min. Qed.
 
-Lemma min_r_iff : forall n m, min n m == m <-> m <= n.
-Proof. intros n m. exact (MPRev.max_l_iff m n). Qed.
+Lemma min_l_iff n m : min n m == n <-> n <= m.
+Proof. solve_min. Qed.
 
-Lemma min_le : forall n m p, min n m <= p -> n <= p \/ m <= p.
-Proof. intros n m p H. destruct (MPRev.max_le _ _ _ H); auto. Qed.
+Lemma min_r_iff n m : min n m == m <-> m <= n.
+Proof. solve_min. Qed.
 
-Lemma min_le_iff : forall n m p, min n m <= p <-> n <= p \/ m <= p.
-Proof. intros n m p. rewrite (MPRev.max_le_iff m n p); intuition. Qed.
+Lemma min_le n m p : min n m <= p -> n <= p \/ m <= p.
+Proof.
+ destruct (min_spec n m); [left|right]; intuition; order.
+Qed.
+
+Lemma min_le_iff n m p : min n m <= p <-> n <= p \/ m <= p.
+Proof. split. apply min_le. solve_min. Qed.
 
-Lemma min_lt_iff : forall n m p, min n m < p <-> n < p \/ m < p.
-Proof. intros n m p. rewrite (MPRev.max_lt_iff m n p); intuition. Qed.
+Lemma min_lt_iff n m p : min n m < p <-> n < p \/ m < p.
+Proof.
+ destruct (min_spec n m); intuition;
+  order || (right; order) || (left; order).
+Qed.
 
-Lemma min_glb_l : forall n m p, p <= min n m -> p <= n.
-Proof. intros n m. exact (MPRev.max_lub_r m n). Qed.
+Lemma min_glb_l n m p : p <= min n m -> p <= n.
+Proof. solve_min. Qed.
 
-Lemma min_glb_r : forall n m p, p <= min n m -> p <= m.
-Proof. intros n m. exact (MPRev.max_lub_l m n). Qed.
+Lemma min_glb_r n m p : p <= min n m -> p <= m.
+Proof. solve_min. Qed.
 
-Lemma min_glb : forall n m p, p <= n -> p <= m -> p <= min n m.
-Proof. intros. apply MPRev.max_lub; auto. Qed.
+Lemma min_glb n m p : p <= n -> p <= m -> p <= min n m.
+Proof. solve_min. Qed.
 
-Lemma min_glb_iff : forall n m p, p <= min n m <-> p <= n /\ p <= m.
-Proof. intros. rewrite (MPRev.max_lub_iff m n p); intuition. Qed.
+Lemma min_glb_iff n m p : p <= min n m <-> p <= n /\ p <= m.
+Proof. solve_min. Qed.
 
-Lemma min_glb_lt : forall n m p, p < n -> p < m -> p < min n m.
-Proof. intros. apply MPRev.max_lub_lt; auto. Qed.
+Lemma min_glb_lt n m p : p < n -> p < m -> p < min n m.
+Proof. solve_min. Qed.
 
-Lemma min_glb_lt_iff : forall n m p, p < min n m <-> p < n /\ p < m.
-Proof. intros. rewrite (MPRev.max_lub_lt_iff m n p); intuition. Qed.
+Lemma min_glb_lt_iff n m p : p < min n m <-> p < n /\ p < m.
+Proof. solve_min. Qed.
 
-Lemma min_le_compat_l : forall n m p, n <= m -> min p n <= min p m.
-Proof. intros n m. exact (MPRev.max_le_compat_r m n). Qed.
+Lemma min_le_compat_l n m p : n <= m -> min p n <= min p m.
+Proof. intros. apply min_glb_iff. solve_min. Qed.
 
-Lemma min_le_compat_r : forall n m p, n <= m -> min n p <= min m p.
-Proof. intros n m. exact (MPRev.max_le_compat_l m n). Qed.
+Lemma min_le_compat_r n m p : n <= m -> min n p <= min m p.
+Proof. intros. apply min_glb_iff. solve_min. Qed.
 
-Lemma min_le_compat : forall n m p q, n <= m -> p <= q ->
+Lemma min_le_compat n m p q : n <= m -> p <= q ->
  min n p <= min m q.
-Proof. intros. apply MPRev.max_le_compat; auto. Qed.
-
+Proof.
+ intros Hnm Hpq.
+ assert (LE := min_le_compat_l _ _ m Hpq).
+ assert (LE' := min_le_compat_r _ _ p Hnm).
+ order.
+Qed.
 
 (** *** Combined properties of min and max *)
 
-Lemma min_max_absorption : forall n m, max n (min n m) == n.
+Lemma min_max_absorption n m : max n (min n m) == n.
 Proof.
  intros.
  destruct (min_spec n m) as [(C,E)|(C,E)]; rewrite E.
@@ -388,7 +379,7 @@ Proof.
  destruct (max_spec n m); intuition; order.
 Qed.
 
-Lemma max_min_absorption : forall n m, min n (max n m) == n.
+Lemma max_min_absorption n m : min n (max n m) == n.
 Proof.
  intros.
  destruct (max_spec n m) as [(C,E)|(C,E)]; rewrite E.
@@ -398,35 +389,35 @@ Qed.
 
 (** Distributivity *)
 
-Lemma max_min_distr : forall n m p,
+Lemma max_min_distr n m p :
  max n (min m p) == min (max n m) (max n p).
 Proof.
- intros. symmetry. apply min_mono.
+ symmetry. apply min_mono.
  eauto with *.
  repeat red; intros. apply max_le_compat_l; auto.
 Qed.
 
-Lemma min_max_distr : forall n m p,
+Lemma min_max_distr n m p :
  min n (max m p) == max (min n m) (min n p).
 Proof.
- intros. symmetry. apply max_mono.
+ symmetry. apply max_mono.
  eauto with *.
  repeat red; intros. apply min_le_compat_l; auto.
 Qed.
 
 (** Modularity *)
 
-Lemma max_min_modular : forall n m p,
+Lemma max_min_modular n m p :
  max n (min m (max n p)) == min (max n m) (max n p).
 Proof.
- intros. rewrite <- max_min_distr.
+ rewrite <- max_min_distr.
  destruct (max_spec n p) as [(C,E)|(C,E)]; rewrite E; auto with *.
  destruct (min_spec m n) as [(C',E')|(C',E')]; rewrite E'.
  rewrite 2 max_l; try order. rewrite min_le_iff; auto.
  rewrite 2 max_l; try order. rewrite min_le_iff; auto.
 Qed.
 
-Lemma min_max_modular : forall n m p,
+Lemma min_max_modular n m p :
  min n (max m (min n p)) == max (min n m) (min n p).
 Proof.
  intros. rewrite <- min_max_distr.
@@ -438,7 +429,7 @@ Qed.
 
 (** Disassociativity *)
 
-Lemma max_min_disassoc : forall n m p,
+Lemma max_min_disassoc n m p :
  min n (max m p) <= max (min n m) p.
 Proof.
  intros. rewrite min_max_distr.
@@ -447,24 +438,24 @@ Qed.
 
 (** Anti-monotonicity swaps the role of [min] and [max] *)
 
-Lemma max_min_antimono : forall f,
+Lemma max_min_antimono f :
  Proper (eq==>eq) f ->
  Proper (le==>inverse le) f ->
  forall x y, max (f x) (f y) == f (min x y).
 Proof.
- intros f Eqf Lef x y.
+ intros Eqf Lef x y.
  destruct (min_spec x y) as [(H,E)|(H,E)]; rewrite E;
   destruct (max_spec (f x) (f y)) as [(H',E')|(H',E')]; auto.
  assert (f y <= f x) by (apply Lef; order). order.
  assert (f x <= f y) by (apply Lef; order). order.
 Qed.
 
-Lemma min_max_antimono : forall f,
+Lemma min_max_antimono f :
  Proper (eq==>eq) f ->
  Proper (le==>inverse le) f ->
  forall x y, min (f x) (f y) == f (max x y).
 Proof.
- intros f Eqf Lef x y.
+ intros Eqf Lef x y.
  destruct (max_spec x y) as [(H,E)|(H,E)]; rewrite E;
   destruct (min_spec (f x) (f y)) as [(H',E')|(H',E')]; auto.
  assert (f y <= f x) by (apply Lef; order). order.
@@ -480,11 +471,11 @@ Module MinMaxDecProperties (Import O:OrderedTypeFull')(Import M:HasMinMax O).
 
 (** Induction principles for [max]. *)
 
-Lemma max_case_strong : forall n m (P:t -> Type),
+Lemma max_case_strong n m (P:t -> Type) :
   (forall x y, x==y -> P x -> P y) ->
   (m<=n -> P n) -> (n<=m -> P m) -> P (max n m).
 Proof.
-intros n m P Compat Hl Hr.
+intros Compat Hl Hr.
 destruct (CompSpec2Type (compare_spec n m)) as [EQ|LT|GT].
 assert (n<=m) by (rewrite le_lteq; auto).
 apply (Compat m), Hr; auto. symmetry; apply max_r; auto.
@@ -494,26 +485,26 @@ assert (m<=n) by (rewrite le_lteq; auto).
 apply (Compat n), Hl; auto. symmetry; apply max_l; auto.
 Defined.
 
-Lemma max_case : forall n m (P:t -> Type),
+Lemma max_case n m (P:t -> Type) :
   (forall x y, x == y -> P x -> P y) ->
   P n -> P m -> P (max n m).
 Proof. intros. apply max_case_strong; auto. Defined.
 
 (** [max] returns one of its arguments. *)
 
-Lemma max_dec : forall n m, {max n m == n} + {max n m == m}.
+Lemma max_dec n m : {max n m == n} + {max n m == m}.
 Proof.
- intros n m. apply max_case; auto with relations.
+ apply max_case; auto with relations.
  intros x y H [E|E]; [left|right]; rewrite <-H; auto.
 Defined.
 
 (** Idem for [min] *)
 
-Lemma min_case_strong : forall n m (P:O.t -> Type),
+Lemma min_case_strong n m (P:O.t -> Type) :
  (forall x y, x == y -> P x -> P y) ->
  (n<=m -> P n) -> (m<=n -> P m) -> P (min n m).
 Proof.
-intros n m P Compat Hl Hr.
+intros Compat Hl Hr.
 destruct (CompSpec2Type (compare_spec n m)) as [EQ|LT|GT].
 assert (n<=m) by (rewrite le_lteq; auto).
 apply (Compat n), Hl; auto. symmetry; apply min_l; auto.
@@ -523,12 +514,12 @@ assert (m<=n) by (rewrite le_lteq; auto).
 apply (Compat m), Hr; auto. symmetry; apply min_r; auto.
 Defined.
 
-Lemma min_case : forall n m (P:O.t -> Type),
+Lemma min_case n m (P:O.t -> Type) :
   (forall x y, x == y -> P x -> P y) ->
   P n -> P m -> P (min n m).
 Proof. intros. apply min_case_strong; auto. Defined.
 
-Lemma min_dec : forall n m, {min n m == n} + {min n m == m}.
+Lemma min_dec n m : {min n m == n} + {min n m == m}.
 Proof.
  intros. apply min_case; auto with relations.
  intros x y H [E|E]; [left|right]; rewrite <- E; auto with relations.
@@ -558,19 +549,19 @@ Module UsualMinMaxLogicalProperties
 
  Include MinMaxLogicalProperties O M.
 
- Lemma max_monotone : forall f, Proper (le ==> le) f ->
+ Lemma max_monotone f : Proper (le ==> le) f ->
   forall x y, max (f x) (f y) = f (max x y).
  Proof. intros; apply max_mono; auto. congruence. Qed.
 
- Lemma min_monotone : forall f, Proper (le ==> le) f ->
+ Lemma min_monotone f : Proper (le ==> le) f ->
   forall x y, min (f x) (f y) = f (min x y).
  Proof. intros; apply min_mono; auto. congruence. Qed.
 
- Lemma min_max_antimonotone : forall f, Proper (le ==> inverse le) f ->
+ Lemma min_max_antimonotone f : Proper (le ==> inverse le) f ->
   forall x y, min (f x) (f y) = f (max x y).
  Proof. intros; apply min_max_antimono; auto. congruence. Qed.
 
- Lemma max_min_antimonotone : forall f, Proper (le ==> inverse le) f ->
+ Lemma max_min_antimonotone f : Proper (le ==> inverse le) f ->
   forall x y, max (f x) (f y) = f (min x y).
  Proof. intros; apply max_min_antimono; auto. congruence. Qed.
 
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.
diff --git a/theories/Structures/OrdersTac.v b/theories/Structures/OrdersTac.v
index 66a672c92..68ffc379d 100644
--- a/theories/Structures/OrdersTac.v
+++ b/theories/Structures/OrdersTac.v
@@ -40,16 +40,26 @@ Definition trans_ord o o' :=
 Local Infix "+" := trans_ord.
 
 
-(** ** The requirements of the tactic : [TotalOrder].
+(** ** The tactic requirements : a total order
 
-   [TotalOrder] contains an equivalence [eq],
-   a strict order [lt] total and compatible with [eq], and
-   a larger order [le] synonym for [lt\/eq].
+   We need :
+   - an equivalence [eq],
+   - a strict order [lt] total and compatible with [eq],
+   - a larger order [le] synonym for [lt\/eq].
+
+   This used to be provided here via a [TotalOrder], but
+   for technical reasons related to extraction, we now ask
+   for two sperate parts: relations in a [EqLtLe] + properties in
+   [IsTotalOrder]. Note that [TotalOrder = EqLtLe <+ IsTotalOrder]
 *)
 
+Module Type IsTotalOrder (O:EqLtLe) :=
+ IsEq O <+ IsStrOrder O <+ LeIsLtEq O <+ LtIsTotal O.
+
 (** ** Properties that will be used by the [order] tactic *)
 
-Module OrderFacts(Import O:TotalOrder').
+Module OrderFacts (Import O:EqLtLe)(P:IsTotalOrder O).
+Include EqLtLeNotation O.
 
 (** Reflexivity rules *)
 
@@ -57,7 +67,7 @@ Lemma eq_refl : forall x, x==x.
 Proof. reflexivity. Qed.
 
 Lemma le_refl : forall x, x<=x.
-Proof. intros; rewrite le_lteq; right; reflexivity. Qed.
+Proof. intros; rewrite P.le_lteq; right; reflexivity. Qed.
 
 Lemma lt_irrefl : forall x, ~ x<x.
 Proof. intros; apply StrictOrder_Irreflexive. Qed.
@@ -69,7 +79,7 @@ Proof. auto with *. Qed.
 
 Lemma le_antisym : forall x y, x<=y -> y<=x -> x==y.
 Proof.
- intros x y; rewrite 2 le_lteq. intuition.
+ intros x y; rewrite 2 P.le_lteq. intuition.
  elim (StrictOrder_Irreflexive x); transitivity y; auto.
 Qed.
 
@@ -90,7 +100,7 @@ Local Notation "#" := interp_ord.
 
 Lemma trans : forall o o' x y z, #o x y -> #o' y z -> #(o+o') x z.
 Proof.
-destruct o, o'; simpl; intros x y z; rewrite ?le_lteq; intuition;
+destruct o, o'; simpl; intros x y z; rewrite ?P.le_lteq; intuition;
  subst_eqns; eauto using (StrictOrder_Transitive x y z) with *.
 Qed.
 
@@ -114,19 +124,19 @@ Proof. eauto using eq_trans, eq_sym. Qed.
 
 Lemma not_neq_eq : forall x y, ~~x==y -> x==y.
 Proof.
-intros x y H. destruct (lt_total x y) as [H'|[H'|H']]; auto;
+intros x y H. destruct (P.lt_total x y) as [H'|[H'|H']]; auto;
  destruct H; intro H; rewrite H in H'; eapply lt_irrefl; eauto.
 Qed.
 
 Lemma not_ge_lt : forall x y, ~y<=x -> x<y.
 Proof.
-intros x y H. destruct (lt_total x y); auto.
-destruct H. rewrite le_lteq. intuition.
+intros x y H. destruct (P.lt_total x y); auto.
+destruct H. rewrite P.le_lteq. intuition.
 Qed.
 
 Lemma not_gt_le : forall x y, ~y<x -> x<=y.
 Proof.
-intros x y H. rewrite le_lteq. generalize (lt_total x y); intuition.
+intros x y H. rewrite P.le_lteq. generalize (P.lt_total x y); intuition.
 Qed.
 
 Lemma le_neq_lt : forall x y, x<=y -> ~x==y -> x<y.
@@ -138,9 +148,9 @@ End OrderFacts.
 
 (** ** [MakeOrderTac] : The functor providing the order tactic. *)
 
-Module MakeOrderTac (Import O:TotalOrder').
-
-Include OrderFacts O.
+Module MakeOrderTac (Import O:EqLtLe)(P:IsTotalOrder O).
+Include OrderFacts O P.
+Include EqLtLeNotation O.
 
 (** order_eq : replace x by y in all (in)equations hyps thanks
    to equality EQ (where eq has been hidden in order to avoid
@@ -257,37 +267,10 @@ End MakeOrderTac.
 
 Module OTF_to_OrderTac (OTF:OrderedTypeFull).
  Module TO := OTF_to_TotalOrder OTF.
- Include !MakeOrderTac TO.
+ Include !MakeOrderTac OTF TO.
 End OTF_to_OrderTac.
 
 Module OT_to_OrderTac (OT:OrderedType).
  Module OTF := OT_to_Full OT.
  Include !OTF_to_OrderTac OTF.
 End OT_to_OrderTac.
-
-Module TotalOrderRev (O:TotalOrder) <: TotalOrder.
-
-Definition t := O.t.
-Definition eq := O.eq.
-Definition lt := flip O.lt.
-Definition le := flip O.le.
-Include EqLtLeNotation.
-
-(* No Instance syntax to avoid saturating the Equivalence tables *)
-Definition eq_equiv := O.eq_equiv.
-
-Instance lt_strorder: StrictOrder lt.
-Proof. unfold lt; auto with *. Qed.
-Instance lt_compat : Proper (eq==>eq==>iff) lt.
-Proof. unfold lt; auto with *. Qed.
-
-Lemma le_lteq : forall x y, x<=y <-> x<y \/ x==y.
-Proof. intros; unfold le, lt, flip. rewrite O.le_lteq; intuition. Qed.
-
-Lemma lt_total : forall x y, x<y \/ x==y \/ y<x.
-Proof.
- intros x y; unfold lt, eq, flip.
- generalize (O.lt_total x y); intuition.
-Qed.
-
-End TotalOrderRev.