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

5 files changed, 11 insertions, 9 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index e09ba93f8e..f9485e64cd 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -446,8 +446,8 @@ let resolve_all_evars debug m env p oevd do_split fail =
 	  | None -> 
 	      if fail then 
 		(* Unable to satisfy the constraints. *)
-		let evm =  evd in
-		let evm = if do_split then select_evars comp evm else evm in
+		let evm = if do_split then select_evars comp evd else evd in
+		let evm = Evarutil.nf_evars evm in
 		let _, ev = Evd.fold 
 		  (fun ev evi (b,acc) -> 
 		    (* focus on one instance if only one was searched for *)
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index 7d6e1de1e6..3e2eb4f40a 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -21,6 +21,10 @@ Require Import Coq.Program.Basics.
 
 Typeclasses Opaque id const flip compose arrow impl iff not all.
 
+(** Apply using the same opacity information as typeclass proof search. *)
+
+Ltac class_apply c := autoapply c using typeclass_instances.
+
 (** The unconvertible typeclass, to test that two objects of the same type are 
    actually different. *)
 
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index ee3d7876dc..19c360f62f 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. *)
 
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 681bd90a9e..1a966ded5f 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -45,7 +45,7 @@ Class Reflexive {A} (R : relation A) :=
 Class Irreflexive {A} (R : relation A) := 
   irreflexivity : Reflexive (complement R).
 
-Hint Extern 1 (Reflexive (complement _)) => eapply @irreflexivity : typeclasses_instances.
+Hint Extern 1 (Reflexive (complement _)) => class_apply @irreflexivity : typeclasses_instances.
 
 Class Symmetric {A} (R : relation A) := 
   symmetry : forall x y, R x y -> R y x.
@@ -311,7 +311,7 @@ Notation "∙⊥∙" := false_predicate : predicate_scope.
 (** Predicate equivalence is an equivalence, and predicate implication defines a preorder. *)
 
 Program Instance predicate_equivalence_equivalence : Equivalence (@predicate_equivalence l).
-  Next Obligation.
+  Next Obligation. 
     induction l ; firstorder.
   Qed.
   Next Obligation.
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 2d5cd659f7..10283e5295 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -258,6 +258,7 @@ let named_of_rel_context l =
   in ctx
 
 let context ?(hook=fun _ -> ()) l =
+  Impargs.make_manual_implicit_args true;
   let env = Global.env() in
   let evars = ref Evd.empty in
   let (env', fullctx), impls = interp_context_evars evars env l in