From 0a4473f6fb3fbcae3e94fabe3af5318c22239f29 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 28 Apr 2009 16:19:58 +0000
Subject: 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
---
 tactics/class_tactics.ml4 | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

(limited to 'tactics')

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 -> [])
-- 
cgit v1.2.3