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, 2 insertions, 2 deletions

diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index 3b2a372ec9..a2bc5e2663 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.