Fixes for bugs in r12110:

- [matches] is not parameterized by evars: normalize before calling
conclPattern.
- fix hints in Morphisms for subrelation and handling of signature
normalization.


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

2 files changed, 6 insertions, 13 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index c6d223a249..222efb54ea 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -117,12 +117,6 @@ let unify_resolve flags (c,clenv) gls =
 
 (** Hack to properly solve dependent evars that are typeclasses *)
 
-let unify_e_resolve flags (c,clenv) =
-  unify_e_resolve flags (c, clenv)
-
-let unify_resolve flags (c,clenv) =
-  unify_resolve flags (c, clenv)
-
 let flags_of_state st =
   {auto_unif_flags with 
     modulo_conv_on_closed_terms = Some st; modulo_delta = st}
@@ -266,7 +260,7 @@ let hints_tac hints =
       (pri, pp, res)
     in
     let tacs =
-      let poss = e_possible_resolve hints info.hints gl.evar_concl in
+      let poss = e_possible_resolve hints info.hints (Evarutil.nf_evar s gl.evar_concl) in
       let l =
 	Util.list_map_append (fun (tac, pri, pptac) ->
 	  try [tac {it = gl; sigma = s}, pri, pptac] with e when catchable e -> [])
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 6029b7cf15..8297b9bd34 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -422,8 +422,8 @@ Proof. firstorder. Qed.
 Lemma inverse2 `(subrelation A R R') : subrelation R (inverse (inverse R')).
 Proof. firstorder. Qed.
 
-Hint Extern 1 (subrelation (flip (flip _)) _) => eapply @inverse1 : typeclass_instances.
-Hint Extern 1 (subrelation _ (flip (flip _))) => eapply @inverse2 : typeclass_instances.
+Hint Extern 1 (subrelation (flip _) _) => eapply @inverse1 : typeclass_instances.
+Hint Extern 1 (subrelation _ (flip _)) => eapply @inverse2 : typeclass_instances.
 
 (** That's if and only if *)
 Instance eq_subrelation `(Reflexive A R) : subrelation (@eq A) R.
@@ -448,18 +448,17 @@ Proof.
   apply H0.
 Qed.
 
-Lemma proper_normalizes_proper `(Proper A R0 m, Normalizes A R0 R1) : Proper R1 m.
+Lemma proper_normalizes_proper `(Normalizes A R0 R1, Proper A R1 m) : Proper R0 m.
 Proof.
   intros A R0 m H R' H'.
-  red in H, H'. setoid_rewrite <- H'.
+  red in H, H'. setoid_rewrite H.
   assumption.
 Qed.
 
 Ltac proper_normalization :=
   match goal with
     | [ _ : normalization_done |- _ ] => fail 1
-    | [ _ : apply_subrelation |- _ ] => fail 1
-    | [ |- @Proper _ ?R _ ] => let H := fresh "H" in
+    | [ _ : apply_subrelation |- @Proper _ ?R _ ] => let H := fresh "H" in
       set(H:=did_normalization) ; eapply @proper_normalizes_proper
   end.