Merge branch 'experimental/upstream' into upstream

1 files changed, 5 insertions, 18 deletions

diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v
index d9b1d76f..c69885b4 100644
--- a/theories/Structures/EqualitiesFacts.v
+++ b/theories/Structures/EqualitiesFacts.v
@@ -8,21 +8,8 @@
 
 Require Import Equalities Bool SetoidList RelationPairs.
 
-(** In a BooleanEqualityType, [eqb] is compatible with [eq] *)
-
-Module BoolEqualityFacts (Import E : BooleanEqualityType).
-
-Instance eqb_compat : Proper (E.eq ==> E.eq ==> Logic.eq) eqb.
-Proof.
-intros x x' Exx' y y' Eyy'.
-apply eq_true_iff_eq.
-rewrite 2 eqb_eq, Exx', Eyy'; auto with *.
-Qed.
-
-End BoolEqualityFacts.
-
-
 (** * Keys and datas used in FMap *)
+
 Module KeyDecidableType(Import D:DecidableType).
 
  Section Elt.
@@ -42,9 +29,9 @@ Module KeyDecidableType(Import D:DecidableType).
 
   (* eqk, eqke are equalities, ltk is a strict order *)
 
-  Global Instance eqk_equiv : Equivalence eqk.
+  Global Instance eqk_equiv : Equivalence eqk := _.
 
-  Global Instance eqke_equiv : Equivalence eqke.
+  Global Instance eqke_equiv : Equivalence eqke := _.
 
   (* Additionnal facts *)
 
@@ -156,7 +143,7 @@ Module PairDecidableType(D1 D2:DecidableType) <: DecidableType.
 
  Definition eq := (D1.eq * D2.eq)%signature.
 
- Instance eq_equiv : Equivalence eq.
+ Instance eq_equiv : Equivalence eq := _.
 
  Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }.
  Proof.
@@ -172,7 +159,7 @@ End PairDecidableType.
 Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType.
  Definition t := (D1.t * D2.t)%type.
  Definition eq := @eq t.
- Program Instance eq_equiv : Equivalence eq.
+ Instance eq_equiv : Equivalence eq := _.
  Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }.
  Proof.
  intros (x1,x2) (y1,y2);