From e4282ea99c664d8d58067bee199cbbcf881b60d5 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sat, 4 Jul 2009 13:28:35 +0200
Subject: Imported Upstream version 8.2.pl1+dfsg

---
 pretyping/pretyping.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'pretyping/pretyping.ml')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 1cac9011..c0f820a2 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pretyping.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
+(* $Id: pretyping.ml 12053 2009-04-06 16:20:42Z msozeau $ *)
 
 open Pp
 open Util
@@ -443,7 +443,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  inh_conv_coerce_to_tycon loc env evdref resj tycon
 	    
     | RLetIn(loc,name,c1,c2)      ->
-	let j = pretype empty_tycon env evdref lvar c1 in
+	let j = 
+	  match c1 with
+	  | RCast (loc, c, CastConv (DEFAULTcast, t)) ->
+	      let tj = pretype_type empty_valcon env evdref lvar t in		
+		pretype (mk_tycon tj.utj_val) env evdref lvar c
+	  | _ -> pretype empty_tycon env evdref lvar c1
+	in
 	let t = refresh_universes j.uj_type in
 	let var = (name,Some j.uj_val,t) in
         let tycon = lift_tycon 1 tycon in
-- 
cgit v1.2.3