diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 10 |
1 files changed, 8 insertions, 2 deletions
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 |