Simplification of OrdersTac thanks to the functor application ! with no inline

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

3 files changed, 7 insertions, 37 deletions

diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v
index 5dec73c62..01c6134b2 100644
--- a/theories/Structures/GenericMinMax.v
+++ b/theories/Structures/GenericMinMax.v
@@ -79,7 +79,7 @@ End GenericMinMax.
 (** ** Consequences of the minimalist interface: facts about [max]. *)
 
 Module MaxLogicalProperties (Import O:TotalOrder')(Import M:HasMax O).
- Module Import T := MakeOrderTac O.
+ Module Import T := !MakeOrderTac O.
 
 (** An alternative caracterisation of [max], equivalent to
     [max_l /\ max_r] *)
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index 7d56d9666..72fbe7968 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -114,12 +114,11 @@ Module OrderedTypeFacts (Import O: OrderedType).
   Definition eq_equiv := eq_equiv.
   Definition lt_strorder := lt_strorder.
   Definition lt_compat := lt_compat.
-  Lemma lt_total : forall x y, lt x y \/ eq x y \/ lt y x.
-  Proof. intros; destruct (compare x y); auto. Qed.
+  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 OrderTac := !MakeOrderTac OrderElts.
   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 35484ae77..64c764d9f 100644
--- a/theories/Structures/OrdersTac.v
+++ b/theories/Structures/OrdersTac.v
@@ -45,38 +45,11 @@ Local Infix "+" := trans_ord.
    [TotalOrder] contains an equivalence [eq],
    a strict order [lt] total and compatible with [eq], and
    a larger order [le] synonym for [lt\/eq].
-
-  NB: we create here a clone of TotalOrder, but without the [Inline] Pragma.
-  This is important for having later the exact shape in Ltac matching.
 *)
 
-Module Type TotalOrder_NoInline <: TotalOrder.
- Parameter Inline t : Type.
- Parameters eq lt le : t -> t -> Prop.
- Include IsEq <+ IsStrOrder <+ LeIsLtEq <+ LtIsTotal.
-End TotalOrder_NoInline.
-
-Module Type TotalOrder_NoInline' := TotalOrder_NoInline <+ EqLtLeNotation.
-
-(** We make explicit aliases to help ltac matching *)
-
-Module CloneOrder (O:TotalOrder_NoInline) <: TotalOrder.
-Definition t := O.t.
-Definition eq := O.eq.
-Definition lt := O.lt.
-Definition le := O.le.
-Definition eq_equiv := O.eq_equiv.
-Definition lt_compat := O.lt_compat.
-Definition lt_strorder := O.lt_strorder.
-Definition le_lteq := O.le_lteq.
-Definition lt_total := O.lt_total.
-End CloneOrder.
-
-
-
 (** ** Properties that will be used by the [order] tactic *)
 
-Module OrderFacts(Import O:TotalOrder_NoInline').
+Module OrderFacts(Import O:TotalOrder').
 
 (** Reflexivity rules *)
 
@@ -165,7 +138,7 @@ End OrderFacts.
 
 (** ** [MakeOrderTac] : The functor providing the order tactic. *)
 
-Module MakeOrderTac (Import O:TotalOrder_NoInline').
+Module MakeOrderTac (Import O:TotalOrder').
 
 Include OrderFacts O.
 
@@ -284,16 +257,14 @@ End MakeOrderTac.
 
 Module OTF_to_OrderTac (OTF:OrderedTypeFull).
  Module TO := OTF_to_TotalOrder OTF.
- Module TO' := CloneOrder TO.
- Include MakeOrderTac TO'.
+ Include !MakeOrderTac TO.
 End OTF_to_OrderTac.
 
 Module OT_to_OrderTac (OT:OrderedType).
  Module OTF := OT_to_Full OT.
- Include OTF_to_OrderTac OTF.
+ Include !OTF_to_OrderTac OTF. (* Why a bang here ? *)
 End OT_to_OrderTac.
 
-(** For example of use of this tactic, see for instance [OrderedType] *)
 
 
 Module TotalOrderRev (O:TotalOrder) <: TotalOrder.