let _note = Printf.sprintf "%s\nSINTH: %s\nEXP: %s"
note (Pp.ppterm csty) (Pp.ppterm cety)
in
+ assert (Ut.is_sober csty);
+ assert (Ut.is_sober cety);
if Ut.alpha_equivalence csty cety then [(* T.Note note *)] else
match name with
| None -> [T.Change (sty, ety, None, e, ""(*note*))]
let rec proc_lambda st name v t =
let dno = DTI.does_not_occur 1 (H.cic t) in
let dno = dno && match get_inner_types st t with
- | None -> true
+ | None -> false
| Some (it, et) ->
DTI.does_not_occur 1 (H.cic it) && DTI.does_not_occur 1 (H.cic et)
in