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

1 files changed, 1 insertions, 7 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 -> [])