6 files changed, 18 insertions, 17 deletions
diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v
index 79e817717..f85222dfb 100644
--- a/theories/Structures/DecidableType.v
+++ b/theories/Structures/DecidableType.v
@@ -80,13 +80,13 @@ Module KeyDecidableType(D:DecidableType).
   Lemma InA_eqke_eqk :
      forall x m, InA eqke x m -> InA eqk x m.
   Proof.
-    unfold eqke; induction 1; intuition.
+    unfold eqke; induction 1; intuition. 
   Qed.
   Hint Resolve InA_eqke_eqk.
 
   Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m.
   Proof.
-   intros; apply InA_eqA with p; auto with *.
+   intros; apply InA_eqA with p; auto with *. 
   Qed.
 
   Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v
index eb5373859..747d03f8a 100644
--- a/theories/Structures/Equalities.v
+++ b/theories/Structures/Equalities.v
@@ -126,14 +126,14 @@ Module Type DecidableTypeFull' := DecidableTypeFull <+ EqNotation.
       [EqualityType] and [DecidableType] *)
 
 Module BackportEq (E:Eq)(F:IsEq E) <: IsEqOrig E.
- Definition eq_refl := @Equivalence_Reflexive _ _ F.eq_equiv.
- Definition eq_sym := @Equivalence_Symmetric _ _ F.eq_equiv.
- Definition eq_trans := @Equivalence_Transitive _ _ F.eq_equiv.
+ Definition eq_refl := F.eq_equiv.(@Equivalence_Reflexive _ _). 
+ Definition eq_sym := F.eq_equiv.(@Equivalence_Symmetric _ _).
+ Definition eq_trans := F.eq_equiv.(@Equivalence_Transitive _ _).
 End BackportEq.
 
 Module UpdateEq (E:Eq)(F:IsEqOrig E) <: IsEq E.
  Instance eq_equiv : Equivalence E.eq.
- Proof. exact (Build_Equivalence _ _ F.eq_refl F.eq_sym F.eq_trans). Qed.
+ Proof. exact (Build_Equivalence _ F.eq_refl F.eq_sym F.eq_trans). Qed.
 End UpdateEq.
 
 Module Backport_ET (E:EqualityType) <: EqualityTypeBoth
diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v
index ffd0649af..a0ee4caaa 100644
--- a/theories/Structures/GenericMinMax.v
+++ b/theories/Structures/GenericMinMax.v
@@ -440,7 +440,7 @@ Qed.
 
 Lemma max_min_antimono f :
  Proper (eq==>eq) f ->
- Proper (le==>inverse le) f ->
+ Proper (le==>flip le) f ->
  forall x y, max (f x) (f y) == f (min x y).
 Proof.
  intros Eqf Lef x y.
@@ -452,7 +452,7 @@ Qed.
 
 Lemma min_max_antimono f :
  Proper (eq==>eq) f ->
- Proper (le==>inverse le) f ->
+ Proper (le==>flip le) f ->
  forall x y, min (f x) (f y) == f (max x y).
 Proof.
  intros Eqf Lef x y.
@@ -557,11 +557,11 @@ Module UsualMinMaxLogicalProperties
   forall x y, min (f x) (f y) = f (min x y).
  Proof. intros; apply min_mono; auto. congruence. Qed.
 
- Lemma min_max_antimonotone f : Proper (le ==> inverse le) f ->
+ Lemma min_max_antimonotone f : Proper (le ==> flip le) f ->
   forall x y, min (f x) (f y) = f (max x y).
  Proof. intros; apply min_max_antimono; auto. congruence. Qed.
 
- Lemma max_min_antimonotone f : Proper (le ==> inverse le) f ->
+ Lemma max_min_antimonotone f : Proper (le ==> flip le) f ->
   forall x y, max (f x) (f y) = f (min x y).
  Proof. intros; apply max_min_antimono; auto. congruence. Qed.
 
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index fa08f9366..fb28e0cfc 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -328,7 +328,7 @@ Module KeyOrderedType(O:OrderedType).
   Proof. split; eauto. Qed.
 
   Global Instance ltk_strorder : StrictOrder ltk.
-  Proof. constructor; eauto. intros x; apply (irreflexivity (x:=fst x)). Qed.
+  Proof. constructor; eauto. intros x; apply (irreflexivity (fst x)). Qed.
 
   Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk.
   Proof.
diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v
index 2e9c0cf56..88fbd8c11 100644
--- a/theories/Structures/OrdersFacts.v
+++ b/theories/Structures/OrdersFacts.v
@@ -31,7 +31,7 @@ Module Type CompareFacts (Import O:DecStrOrder').
 
  Lemma compare_lt_iff x y : (x ?= y) = Lt <-> x<y.
  Proof.
- case compare_spec; intro H; split; try easy; intro LT;
+  case compare_spec; intro H; split; try easy; intro LT;
   contradict LT; rewrite H; apply irreflexivity.
  Qed.
 
@@ -90,7 +90,7 @@ Module Type OrderedTypeFullFacts (Import O:OrderedTypeFull').
  Instance le_order : PartialOrder eq le.
  Proof. compute; iorder. Qed.
 
- Instance le_antisym : Antisymmetric _ eq le.
+ Instance le_antisym : Antisymmetric eq le.
  Proof. apply partial_order_antisym; auto with *. Qed.
 
  Lemma le_not_gt_iff : forall x y, x<=y <-> ~y<x.
diff --git a/theories/Structures/OrdersTac.v b/theories/Structures/OrdersTac.v
index 68ffc379d..475a25a41 100644
--- a/theories/Structures/OrdersTac.v
+++ b/theories/Structures/OrdersTac.v
@@ -29,7 +29,7 @@ Set Implicit Arguments.
     [le x y -> le y z -> le x z].
 *)
 
-Inductive ord := OEQ | OLT | OLE.
+Inductive ord : Set := OEQ | OLT | OLE.
 Definition trans_ord o o' :=
  match o, o' with
  | OEQ, _ => o'
@@ -70,7 +70,7 @@ Lemma le_refl : forall x, x<=x.
 Proof. intros; rewrite P.le_lteq; right; reflexivity. Qed.
 
 Lemma lt_irrefl : forall x, ~ x<x.
-Proof. intros; apply StrictOrder_Irreflexive. Qed.
+Proof. intros. apply StrictOrder_Irreflexive. Qed.
 
 (** Symmetry rules *)
 
@@ -100,8 +100,9 @@ Local Notation "#" := interp_ord.
 
 Lemma trans : forall o o' x y z, #o x y -> #o' y z -> #(o+o') x z.
 Proof.
-destruct o, o'; simpl; intros x y z; rewrite ?P.le_lteq; intuition;
- subst_eqns; eauto using (StrictOrder_Transitive x y z) with *.
+destruct o, o'; simpl; intros x y z;
+rewrite ?P.le_lteq; intuition auto;
+subst_eqns; eauto using (StrictOrder_Transitive x y z) with *.
 Qed.
 
 Definition eq_trans x y z : x==y -> y==z -> x==z := @trans OEQ OEQ x y z.