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
+ let sty, ety = H.acic_bc st.context sty, H.acic_bc st.context ety in
match name with
| None -> [T.Change (sty, ety, None, e, ""(*note*))]
| Some (id, i) ->
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
mk_fwd_rewrite st dtext intro tl false v
| v ->
let qs = [proc_proof (next st) v; [T.Id ""]] in
- st, [T.Branch (qs, ""); T.Cut (intro, ity, dtext)]
+ let ity = H.acic_bc st.context ity in
+ st, [T.Branch (qs, ""); T.Cut (intro, ity, dtext)]
in
st, C.Decl (H.cic ity), rqv
| None ->