Merge branch 'subclasses' into coq-trunk

Stop using hnf_constr in unify_type, which might unfold constants
that are marked opaque for unification.
Conflicts:
	pretyping/unification.ml

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

1 files changed, 11 insertions, 5 deletions

diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index f75c9274d..9b8301a5d 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -230,28 +230,34 @@ Hint Extern 4 (subrelation (inverse _) _) =>
 
 (** The complement of a relation conserves its proper elements. *)
 
-Program Instance complement_proper
+Program Definition complement_proper
   `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) :
-  Proper (RA ==> RA ==> iff) (complement R).
+  Proper (RA ==> RA ==> iff) (complement R) := _.
 
-  Next Obligation.
+ Next Obligation.
   Proof.
     unfold complement.
     pose (mR x y H x0 y0 H0).
     intuition.
   Qed.
+ 
+Hint Extern 1 (Proper (_ ==> _ ==> iff) (complement _)) => 
+  apply @complement_proper : typeclass_instances.
 
 (** The [inverse] too, actually the [flip] instance is a bit more general. *)
 
-Program Instance flip_proper
+Program Definition flip_proper
   `(mor : Proper (A -> B -> C) (RA ==> RB ==> RC) f) :
-  Proper (RB ==> RA ==> RC) (flip f).
+  Proper (RB ==> RA ==> RC) (flip f) := _.
 
   Next Obligation.
   Proof.
     apply mor ; auto.
   Qed.
 
+Hint Extern 1 (Proper (_ ==> _ ==> _) (flip _)) => 
+  apply @flip_proper : typeclass_instances.
+
 (** Every Transitive relation gives rise to a binary morphism on [impl],
    contravariant in the first argument, covariant in the second. *)