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) ->
compute_letin_type context te,
List.map (fun x -> compute_letin_type context x) pl)
| C.Fix (fno,fl) ->
+ let fl =
+ List.map
+ (function (name,recno,ty,bo) ->
+ name,recno,compute_letin_type context ty, bo) fl in
let tys,_ =
List.fold_left
(fun (types,len) (n,_,ty,_) ->
C.Fix (fno,
List.map
(fun (name,recno,ty,bo) ->
- name, recno,
- compute_letin_type context ty,
- compute_letin_type (tys @ context) bo
+ name, recno, ty, compute_letin_type (tys @ context) bo
) fl)
| C.CoFix (fno,fl) ->
+ let fl =
+ List.map
+ (function (name,ty,bo) ->
+ name, compute_letin_type context ty, bo) fl in
let tys,_ =
List.fold_left
(fun (types,len) (n,ty,_) ->
C.CoFix (fno,
List.map
(fun (name,ty,bo) ->
- name,
- compute_letin_type context ty,
- compute_letin_type (tys @ context) bo
+ name, ty, compute_letin_type (tys @ context) bo
) fl)
;;