From ec26ef7bdee30f93b53d53171fc881f8413cb7c1 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 11 Jun 2009 00:51:32 +0000
Subject: When typing a non-dependent arrow, do not put the (anonymous)
 variable in the context to avoid it being abstracted over in potential evars
 occuring in the codomain, which can prevent unifications. Add [intro] to the
 typeclasses eauto and fix [make_resolve_hyp] to properly normalize types
 w.r.t. evars before searching for a class in an hypothesis.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12182 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/class_tactics.ml4 | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 6fdd8c2827..8f548210b8 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -335,6 +335,7 @@ let is_transparent_gr (ids, csts) = function
   | IndRef _ | ConstructRef _ -> false
 
 let make_resolve_hyp env sigma st flags pri (id, _, cty) =
+  let cty = Evarutil.nf_evar sigma cty in
   let ctx, ar = decompose_prod cty in
   let keep = 
     match kind_of_term (fst (decompose_app ar)) with
@@ -379,7 +380,7 @@ let eauto hints g =
 	{it = List.map fst goals; sigma = s}, valid s
 
 let real_eauto st hints p evd =
-  let tac = fix (hints_tac hints) in
+  let tac = fix (or_tac intro_tac (hints_tac hints)) in
   let rec aux evd =
     match run_on_evars ~st p evd tac with
     | None -> evd
-- 
cgit v1.2.3