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

3 files changed, 19 insertions, 19 deletions

diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index 408461a25..477c431c4 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -1752,27 +1752,27 @@ Hint Unfold flip.
 
 (** Correctness of this comparison *)
 
-Definition LCmp c x y := Cmp L.eq L.lt x y c.
+Definition Cmp c x y := CompSpec L.eq L.lt x y c.
 
-Hint Unfold LCmp.
+Hint Unfold Cmp.
 
 Lemma compare_end_Cmp :
- forall e2, LCmp (compare_end e2) nil (flatten_e e2).
+ forall e2, Cmp (compare_end e2) nil (flatten_e e2).
 Proof.
  destruct e2; simpl; constructor; auto. reflexivity.
 Qed.
 
 Lemma compare_more_Cmp : forall x1 cont x2 r2 e2 l,
-  LCmp (cont (cons r2 e2)) l (elements r2 ++ flatten_e e2) ->
-   LCmp (compare_more x1 cont (More x2 r2 e2)) (x1::l)
+  Cmp (cont (cons r2 e2)) l (elements r2 ++ flatten_e e2) ->
+   Cmp (compare_more x1 cont (More x2 r2 e2)) (x1::l)
       (flatten_e (More x2 r2 e2)).
 Proof.
  simpl; intros; elim_compare x1 x2; simpl; auto.
 Qed.
 
 Lemma compare_cont_Cmp : forall s1 cont e2 l,
- (forall e, LCmp (cont e) l (flatten_e e)) ->
- LCmp (compare_cont s1 cont e2) (elements s1 ++ l) (flatten_e e2).
+ (forall e, Cmp (cont e) l (flatten_e e)) ->
+ Cmp (compare_cont s1 cont e2) (elements s1 ++ l) (flatten_e e2).
 Proof.
  induction s1 as [|l1 Hl1 x1 r1 Hr1 h1]; simpl; intros; auto.
  rewrite <- elements_node; simpl.
@@ -1783,7 +1783,7 @@ Proof.
 Qed.
 
 Lemma compare_Cmp : forall s1 s2,
- LCmp (compare s1 s2) (elements s1) (elements s2).
+ Cmp (compare s1 s2) (elements s1) (elements s2).
 Proof.
  intros; unfold compare.
  rewrite (app_nil_end (elements s1)).
@@ -1795,7 +1795,7 @@ Proof.
 Qed.
 
 Lemma compare_spec : forall s1 s2 `{Ok s1, Ok s2},
- Cmp eq lt s1 s2 (compare s1 s2).
+ CompSpec eq lt s1 s2 (compare s1 s2).
 Proof.
  intros.
  destruct (compare_Cmp s1 s2); constructor.
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index a011eb32e..ef32c114b 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -227,7 +227,7 @@ Module Type SetsOn (E : OrderedType).
   Variable s s': t.
   Variable x y : elt.
 
-  Parameter compare_spec : Cmp eq lt s s' (compare s s').
+  Parameter compare_spec : CompSpec eq lt s s' (compare s s').
 
   (** Additional specification of [elements] *)
   Parameter elements_spec2 : sort E.lt (elements s).
@@ -570,7 +570,7 @@ Module Type RawSets (E : OrderedType).
   Variable x y : elt.
 
   (** Specification of [compare] *)
-  Parameter compare_spec : forall `{Ok s, Ok s'}, Cmp eq lt s s' (compare s s').
+  Parameter compare_spec : forall `{Ok s, Ok s'}, CompSpec eq lt s s' (compare s s').
 
   (** Additional specification of [elements] *)
   Parameter elements_spec2 : forall `{Ok s}, sort E.lt (elements s).
@@ -619,7 +619,7 @@ Module Raw2SetsOn (O:OrderedType)(M:RawSets O) <: SetsOn O.
   Variable s s' s'' : t.
   Variable x y : elt.
 
-  Lemma compare_spec : Cmp eq lt s s' (compare s s').
+  Lemma compare_spec : CompSpec eq lt s s' (compare s s').
   Proof.
    assert (H:=@M.compare_spec s s' _ _).
    unfold compare; destruct M.compare; inversion_clear H; auto.
@@ -940,11 +940,11 @@ Module MakeListOrdering (O:OrderedType).
  Qed.
  Hint Resolve eq_cons.
 
- Lemma cons_Cmp : forall c x1 x2 l1 l2, O.eq x1 x2 ->
-  Cmp eq lt l1 l2 c -> Cmp eq lt (x1::l1) (x2::l2) c.
+ Lemma cons_CompSpec : forall c x1 x2 l1 l2, O.eq x1 x2 ->
+  CompSpec eq lt l1 l2 c -> CompSpec eq lt (x1::l1) (x2::l2) c.
  Proof.
   destruct c; simpl; inversion_clear 2; auto.
  Qed.
- Hint Resolve cons_Cmp.
+ Hint Resolve cons_CompSpec.
 
 End MakeListOrdering.
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index 28205e3f6..8b0a16c11 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -790,20 +790,20 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
    split; auto. transitivity s4; auto.
   Qed.
 
-  Lemma compare_spec_aux : forall s s', Cmp eq L.lt s s' (compare s s').
+  Lemma compare_spec_aux : forall s s', CompSpec eq L.lt s s' (compare s s').
   Proof.
   induction s as [|x s IH]; intros [|x' s']; simpl; intuition.
   elim_compare x x'; auto.
   Qed.
 
   Lemma compare_spec : forall s s', Ok s -> Ok s' ->
-   Cmp eq lt s s' (compare s s').
+   CompSpec eq lt s s' (compare s s').
   Proof.
   intros s s' Hs Hs'.
   generalize (compare_spec_aux s s').
   destruct (compare s s'); inversion_clear 1; auto.
-  apply Cmp_lt. exists s, s'; repeat split; auto using @ok.
-  apply Cmp_gt. exists s', s; repeat split; auto using @ok.
+  apply CompLt. exists s, s'; repeat split; auto using @ok.
+  apply CompGt. exists s', s; repeat split; auto using @ok.
   Qed.
 
 End MakeRaw.