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
---
 pretyping/pretyping.ml    | 12 +++++++++---
 tactics/class_tactics.ml4 |  3 ++-
 2 files changed, 11 insertions(+), 4 deletions(-)

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 8c06f9bfec..bc0dba8831 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -434,9 +434,15 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 
     | RProd(loc,name,bk,c1,c2)        ->
 	let j = pretype_type empty_valcon env evdref lvar c1 in
-	let var = (name,j.utj_val) in
-	let env' = push_rel_assum var env in
-	let j' = pretype_type empty_valcon env' evdref lvar c2 in
+	let j' =
+	  if name = Anonymous then
+	    let j = pretype_type empty_valcon env evdref lvar c2 in
+	      { j with utj_val = lift 1 j.utj_val }
+	  else
+	    let var = (name,j.utj_val) in
+	    let env' = push_rel_assum var env in
+	      pretype_type empty_valcon env' evdref lvar c2
+	in
 	let resj =
 	  try judge_of_product env name j j'
 	  with TypeError _ as e -> Stdpp.raise_with_loc loc e in
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