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

2 files changed, 5 insertions, 9 deletions

diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 37074aba5..5582438b7 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -147,18 +147,14 @@ Definition lt_total := lt_trichotomy.
 Definition le_lteq := lt_eq_cases.
 
 Module Private_OrderTac.
-Module Elts <: TotalOrder.
- Definition t := t.
- Definition eq := eq.
- Definition lt := lt.
- Definition le := le.
+Module IsTotal.
  Definition eq_equiv := eq_equiv.
  Definition lt_strorder := lt_strorder.
  Definition lt_compat := lt_compat.
  Definition lt_total := lt_total.
  Definition le_lteq := le_lteq.
-End Elts.
-Module Tac := !MakeOrderTac Elts.
+End IsTotal.
+Module Tac := !MakeOrderTac NZ IsTotal.
 End Private_OrderTac.
 Ltac order := Private_OrderTac.Tac.order.
 
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index 3b2a372ec..a2bc5e266 100644
--- a/theories/Numbers/Rational/BigQ/BigQ.v
+++ b/theories/Numbers/Rational/BigQ/BigQ.v
@@ -42,6 +42,7 @@ Module BigQ <: QType <: OrderedTypeFull <: TotalOrder.
  Bind Scope bigQ_scope with t t_.
  Include !QProperties <+ HasEqBool2Dec
   <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties.
+ Ltac order := Private_Tac.order.
 End BigQ.
 
 (** Notations about [BigQ] *)
@@ -144,8 +145,7 @@ End TestField.
 
 (** [BigQ] can also benefit from an "order" tactic *)
 
-Module BigQ_Order := !OrdersTac.MakeOrderTac BigQ.
-Ltac bigQ_order := BigQ_Order.order.
+Ltac bigQ_order := BigQ.order.
 
 Section TestOrder.
 Let test : forall x y : bigQ, x<=y -> y<=x -> x==y.