- 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, 3 insertions, 3 deletions

diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v
index 7972c96ca..0fa5bfaa6 100644
--- a/theories/Classes/RelationPairs.v
+++ b/theories/Classes/RelationPairs.v
@@ -88,10 +88,10 @@ Section RelCompFun_Instances.
     `(Measure A B f, Irreflexive _ R) : Irreflexive (R@@f).
   Proof. firstorder. Qed.
 
-  Global Instance RelCompFun_Equivalence
+  Global Program Instance RelCompFun_Equivalence
     `(Measure A B f, Equivalence _ R) : Equivalence (R@@f).
 
-  Global Instance RelCompFun_StrictOrder
+  Global Program Instance RelCompFun_StrictOrder
     `(Measure A B f, StrictOrder _ R) : StrictOrder (R@@f).
 
 End RelCompFun_Instances.
@@ -108,7 +108,7 @@ Instance RelProd_Transitive {A B}(RA:relation A)(RB:relation B)
  `(Transitive _ RA, Transitive _ RB) : Transitive (RA*RB).
 Proof. firstorder. Qed.
 
-Instance RelProd_Equivalence {A B}(RA:relation A)(RB:relation B)
+Program Instance RelProd_Equivalence {A B}(RA:relation A)(RB:relation B)
  `(Equivalence _ RA, Equivalence _ RB) : Equivalence (RA*RB).
 
 Lemma FstRel_ProdRel {A B}(RA:relation A) :