- | None -> []
- | Some (sty, ety) ->
- let e = Cn.hole "" in
- let csty, cety = cic sty, cic ety in
- if Ut.alpha_equivalence csty cety then [] else
- match name with
- | 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, Some id), e, "")]
- end
-
+ | None -> [(*T.Note "NORMAL: NO INNER TYPES"*)]
+ | Some (sty, ety) -> mk_convert st ?name sty ety "NORMAL"
+
+let convert_elim st ?name t v pattern =
+ match t, get_inner_types st t, get_inner_types st v with
+ | _, None, _
+ | _, _, None -> [(* T.Note "ELIM: NO INNER TYPES"*)]
+ | C.AAppl (_, hd :: tl), Some (tsty, _), Some (vsty, _) ->
+ let where = List.hd (List.rev tl) in
+ let cty = Cn.elim_inferred_type
+ st.context (H.cic vsty) (H.cic where) (H.cic hd) (H.cic pattern)
+ in
+ mk_convert st ?name (Cn.fake_annotate "" st.context cty) tsty "ELIM"
+ | _, Some _, Some _ -> assert false
+