(compute_letin_type context te,
compute_letin_type context ty)
| C.Prod (name,so,dest) ->
- C.Prod (name,
- compute_letin_type context so,
+ let so = compute_letin_type context so in
+ C.Prod (name, so,
compute_letin_type ((Some (name,(C.Decl so)))::context) dest)
| C.Lambda (name,so,dest) ->
- C.Lambda (name,
- compute_letin_type context so,
+ let so = compute_letin_type context so in
+ C.Lambda (name, so,
compute_letin_type ((Some (name,(C.Decl so)))::context) dest)
| C.LetIn (name,so,C.Implicit _,dest) ->
- let ty = !type_of_aux' context so in
- C.LetIn (name,
- compute_letin_type context so,
- ty,
+ let so = compute_letin_type 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) ->
- C.LetIn (name,
- compute_letin_type context so,
- compute_letin_type context ty,
+ let so = compute_letin_type context so in
+ let ty = compute_letin_type context ty in
+ C.LetIn (name, so, ty,
compute_letin_type ((Some (name,(C.Def (so,ty))))::context) dest)
| C.Appl l ->
C.Appl (List.map (fun x -> compute_letin_type context x) l)
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)
;;