- | None -> [T.Change (st, et, None, e, "")]
- | Some id -> [T.Change (st, et, Some (id, id), e, ""); T.ClearBody (id, "")]
+ | None -> [T.Change (sty, ety, None, e, "")]
+ | Some (id, i) ->
+ begin match get_entry st id with
+ | C.Def _ -> [T.ClearBody (id, "")]
+ | C.Decl w ->
+ let w = S.lift i w in
+ if Ut.alpha_equivalence csty w then []
+ else
+ [T.Note (Pp.ppterm csty); T.Note (Pp.ppterm w);
+ T.Change (sty, ety, Some (id, id), e, "")]
+ end