- 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/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.