- Add modulo_delta_types flag for unification to allow full

conversion when checking types of instanciations while having
restricted delta reduction for unification itself. This
makes auto/eauto... backward compatible.
- Change semantics of [Instance foo : C a.] to _not_ search
for an instance of [C a] automatically and potentially slow
down interaction, except for trivial classes with no fields.
Use [C a := _.] or [C a := {}] to search for an instance of
the class or for every field.
- Correct treatment of transparency information for classes 
declared in sections.


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

1 files changed, 4 insertions, 4 deletions

diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v
index d8a1b7581..c69885b46 100644
--- a/theories/Structures/EqualitiesFacts.v
+++ b/theories/Structures/EqualitiesFacts.v
@@ -29,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 *)
 
@@ -143,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.
@@ -159,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);