- 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

9 files changed, 19 insertions, 19 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) :
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index c81a72f89..206714949 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -494,9 +494,9 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
 
   Definition lt_key (p p':positive*A) := E.lt (fst p) (fst p').
 
-  Global Instance eqk_equiv : Equivalence eq_key.
-  Global Instance eqke_equiv : Equivalence eq_key_elt.
-  Global Instance ltk_strorder : StrictOrder lt_key.
+  Global Program Instance eqk_equiv : Equivalence eq_key.
+  Global Program Instance eqke_equiv : Equivalence eq_key_elt.
+  Global Program Instance ltk_strorder : StrictOrder lt_key.
 
   Lemma mem_find :
     forall m x, mem x m = match find x m with None => false | _ => true end.
diff --git a/theories/FSets/FSetCompat.v b/theories/FSets/FSetCompat.v
index c3d614eeb..6b3d86d39 100644
--- a/theories/FSets/FSetCompat.v
+++ b/theories/FSets/FSetCompat.v
@@ -264,7 +264,7 @@ Module Update_WSets
  Instance In_compat : Proper (E.eq==>Logic.eq==>iff) In.
  Proof. intros x x' Hx s s' Hs. subst. apply MF.In_eq_iff; auto. Qed.
 
- Instance eq_equiv : Equivalence eq.
+ Instance eq_equiv : Equivalence eq := _.
 
  Section Spec.
   Variable s s': t.
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.
 
diff --git a/theories/Numbers/Rational/SpecViaQ/QSig.v b/theories/Numbers/Rational/SpecViaQ/QSig.v
index 2bdc1bba2..a4f0dbce1 100644
--- a/theories/Numbers/Rational/SpecViaQ/QSig.v
+++ b/theories/Numbers/Rational/SpecViaQ/QSig.v
@@ -115,7 +115,7 @@ Ltac solve_wd2 := intros x x' Hx y y' Hy; qify; now rewrite Hx, Hy.
 Local Obligation Tactic := solve_wd2 || solve_wd1.
 
 Instance : Measure to_Q.
-Instance eq_equiv : Equivalence eq.
+Instance eq_equiv : Equivalence eq := {}.
 
 Program Instance lt_wd : Proper (eq==>eq==>iff) lt.
 Program Instance le_wd : Proper (eq==>eq==>iff) le.
@@ -141,7 +141,7 @@ Proof. intros. qify. destruct (Qcompare_spec [x] [y]); auto. Qed.
 (** Let's implement [TotalOrder] *)
 
 Definition lt_compat := lt_wd.
-Instance lt_strorder : StrictOrder lt.
+Instance lt_strorder : StrictOrder lt := {}.
 
 Lemma le_lteq : forall x y, x<=y <-> x<y \/ x==y.
 Proof. intros. qify. apply Qle_lteq. Qed.
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);
diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v
index a28b79776..b328ae2e8 100644
--- a/theories/Structures/OrdersFacts.v
+++ b/theories/Structures/OrdersFacts.v
@@ -208,7 +208,7 @@ Module OrderedTypeRev (O:OrderedTypeFull) <: OrderedTypeFull.
 
 Definition t := O.t.
 Definition eq := O.eq.
-Instance eq_equiv : Equivalence eq.
+Program Instance eq_equiv : Equivalence eq.
 Definition eq_dec := O.eq_dec.
 
 Definition lt := flip O.lt.
diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v
index 2ed070268..f83b63779 100644
--- a/theories/Structures/OrdersLists.v
+++ b/theories/Structures/OrdersLists.v
@@ -86,11 +86,11 @@ Module KeyOrderedType(Import O:OrderedType).
 
   (* 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 := _.
 
-  Global Instance ltk_strorder : StrictOrder ltk.
+  Global Instance ltk_strorder : StrictOrder ltk := _.
 
   Global Instance ltk_compat : Proper (eqk==>eqk==>iff) ltk.
   Proof. unfold eqk, ltk; auto with *. Qed.