- | Cic.LetIn (name, (s as old_s), t) ->
- let s, fixpoints_s = aux octx ctx n_fix uri s in
- let old_ty,_ =
- CicTypeChecker.type_of_aux' [] octx old_s CicUniv.oblivion_ugraph
- in
- let ty, fixpoints_ty = aux octx ctx n_fix uri old_ty in
- let ctx = Ce (cn_to_s name, NCic.Def (s, ty)) :: ctx in
- let octx = Some (name, Cic.Def (old_s, Some old_ty)) :: octx in
+ | Cic.LetIn (name, (te as old_te), (ty as old_ty), t) ->
+ let te, fixpoints_s = aux octx ctx n_fix uri te in
+ let ty, fixpoints_ty = aux octx ctx n_fix uri ty in
+ let ctx = Ce (cn_to_s name, NCic.Def (te, ty)) :: ctx in
+ let octx = Some (name, Cic.Def (old_te, old_ty)) :: octx in