Minor fixes in typeclasses:

- Set implicit args on for Context decls
- Move class_apply tactic to Init
- Normalize evars before raising an error.


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

1 files changed, 2 insertions, 5 deletions

diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index ee3d7876d..19c360f62 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -101,8 +101,7 @@ Hint Unfold Transitive : core.
 
 Typeclasses Opaque respectful pointwise_relation forall_relation.
 
-Program Instance respectful_per `(PER A (R : relation A), PER B (R' : relation B)) : 
-  PER (R ==> R').
+Program Instance respectful_per `(PER A R, PER B R') : PER (R ==> R').
 
   Next Obligation.
   Proof with auto.
@@ -127,8 +126,6 @@ Proof. simpl_relation. apply subr. apply H. apply subl. apply H0. Qed.
 Lemma subrelation_refl A R : @subrelation A R R.
 Proof. simpl_relation. Qed.
 
-Ltac class_apply c := autoapply c using typeclass_instances.
-
 Ltac subrelation_tac T U := 
   (is_ground T ; is_ground U ; class_apply @subrelation_refl) ||
     class_apply @subrelation_respectful || class_apply @subrelation_refl.
@@ -438,7 +435,7 @@ Hint Extern 1 (subrelation _ (flip _)) => class_apply @inverse2 : typeclass_inst
 Lemma eq_subrelation `(Reflexive A R) : subrelation (@eq A) R.
 Proof. simpl_relation. Qed.
 
-Hint Extern 3 (subrelation (@eq _) ?R) => not_evar R ; class_apply eq_subrelation.
+(* Hint Extern 3 (subrelation (@eq _) ?R) => not_evar R ; class_apply eq_subrelation : typeclass_instances. *)
 
 (** Once we have normalized, we will apply this instance to simplify the problem. *)