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 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

(limited to 'pretyping')

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