compute_letin_type ((Some (name,(C.Decl so)))::context) dest)
| C.LetIn (name,so,C.Implicit _,dest) ->
let so = compute_letin_type context so in
- let ty = !type_of_aux' context so in
+ let ty = Unshare.unshare ~fresh_univs:true (!type_of_aux' context so) in
C.LetIn (name, so, ty,
compute_letin_type ((Some (name,(C.Def (so,ty))))::context) dest)
| C.LetIn (name,so,ty,dest) ->