| C.LetIn (name,so,dest) ->
let _,ty,metasenv,ugraph =
pack_coercions := false;
| C.LetIn (name,so,dest) ->
let _,ty,metasenv,ugraph =
pack_coercions := false;
pack_coercions := true;
let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
pack_coercions := true;
let ctx' = Some (name,(C.Def (so,Some ty)))::ctx in
C.LetIn (name, merge_coercions ctx so, merge_coercions ctx' dest)
let b,_,_,_,_ = is_a_double_coercion t in
(* prerr_endline "CANDIDATO!!!!"; *)
if b then
let b,_,_,_,_ = is_a_double_coercion t in
(* prerr_endline "CANDIDATO!!!!"; *)
if b then