- 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

2 files changed, 2 insertions, 2 deletions

diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index 851237d8f..20504bcf8 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -872,7 +872,7 @@ Module MakeListOrdering (O:OrderedType).
 
  Definition eq s s' := forall x, In x s <-> In x s'.
 
- Instance eq_equiv : Equivalence eq.
+ Instance eq_equiv : Equivalence eq := _.
 
  Inductive lt_list : t -> t -> Prop :=
     | lt_nil : forall x s, lt_list nil (x :: s)
diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v
index 799e5f57e..76f09c76e 100644
--- a/theories/MSets/MSetWeakList.v
+++ b/theories/MSets/MSetWeakList.v
@@ -515,7 +515,7 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
 
   Definition In := InA X.eq.
   Definition eq := Equal.
-  Instance eq_equiv : Equivalence eq.
+  Instance eq_equiv : Equivalence eq := _.
 
 End MakeRaw.