Better visibility of the inductive CompSpec used to specify comparison functions

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

4 files changed, 9 insertions, 17 deletions

diff --git a/theories/Structures/OrderedType2.v b/theories/Structures/OrderedType2.v
index 4d62c2716..310f99a4a 100644
--- a/theories/Structures/OrderedType2.v
+++ b/theories/Structures/OrderedType2.v
@@ -14,14 +14,6 @@ Unset Strict Implicit.
 
 (** * Ordered types *)
 
-Inductive Cmp {A} (eq lt:relation A)(x y : A) : comparison -> Prop :=
-| Cmp_eq : eq x y -> Cmp eq lt x y Eq
-| Cmp_lt : lt x y -> Cmp eq lt x y Lt
-| Cmp_gt : lt y x -> Cmp eq lt x y Gt.
-
-Hint Constructors Cmp.
-
-
 Module Type MiniOrderedType.
   Include Type EqualityType.
 
@@ -29,8 +21,8 @@ Module Type MiniOrderedType.
   Instance lt_strorder : StrictOrder lt.
   Instance lt_compat : Proper (eq==>eq==>iff) lt.
 
-  Parameter compare : t -> t -> comparison.
-  Axiom compare_spec : forall x y, Cmp eq lt x y (compare x y).
+  Parameter Inline compare : t -> t -> comparison.
+  Axiom compare_spec : forall x y, CompSpec eq lt x y (compare x y).
 
 End MiniOrderedType.
 
@@ -76,8 +68,8 @@ Module Type UsualOrderedType.
     for subtyping... *)
  Instance lt_compat : Proper (eq==>eq==>iff) lt.
 
- Parameter compare : t -> t -> comparison.
- Axiom compare_spec : forall x y, Cmp eq lt x y (compare x y).
+ Parameter Inline compare : t -> t -> comparison.
+ Axiom compare_spec : forall x y, CompSpec eq lt x y (compare x y).
 
 End UsualOrderedType.
 
diff --git a/theories/Structures/OrderedType2Alt.v b/theories/Structures/OrderedType2Alt.v
index 4e14f5128..43b27553f 100644
--- a/theories/Structures/OrderedType2Alt.v
+++ b/theories/Structures/OrderedType2Alt.v
@@ -76,7 +76,7 @@ Module Update_OT (O:OrderedTypeOrig) <: OrderedType.
     | GT _ => Gt
   end.
 
- Lemma compare_spec : forall x y, Cmp eq lt x y (compare x y).
+ Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
  Proof.
   intros; unfold compare; destruct O.compare; auto.
  Qed.
@@ -169,11 +169,11 @@ Module OT_from_Alt (Import O:OrderedTypeAlt) <: OrderedType.
 
  Definition compare := O.compare.
 
- Lemma compare_spec : forall x y, Cmp eq lt x y (compare x y).
+ Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
  Proof.
   unfold eq, lt, compare; intros.
   destruct (O.compare x y) as [ ]_eqn:H; auto.
-  apply Cmp_gt.
+  apply CompGt.
   rewrite compare_sym, H; auto.
  Qed.
 
diff --git a/theories/Structures/OrderedType2Ex.v b/theories/Structures/OrderedType2Ex.v
index 801c18723..6a0231973 100644
--- a/theories/Structures/OrderedType2Ex.v
+++ b/theories/Structures/OrderedType2Ex.v
@@ -77,7 +77,7 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType.
    | Gt => Gt
   end.
 
- Lemma compare_spec : forall x y, Cmp eq lt x y (compare x y).
+ Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
  Proof.
  intros (x1,x2) (y1,y2); unfold compare; simpl.
  destruct (O1.compare_spec x1 y1); try (constructor; compute; auto).
diff --git a/theories/Structures/OrderedType2Facts.v b/theories/Structures/OrderedType2Facts.v
index 382b6366d..a7bb661ea 100644
--- a/theories/Structures/OrderedType2Facts.v
+++ b/theories/Structures/OrderedType2Facts.v
@@ -254,7 +254,7 @@ Proof. intros; unfold le, lt, flip. rewrite O.le_lteq; intuition. Qed.
 
 Definition compare := flip O.compare.
 
-Lemma compare_spec : forall x y, Cmp eq lt x y (compare x y).
+Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
 Proof.
 intros; unfold compare, eq, lt, flip.
 destruct (O.compare_spec y x); auto.