+let used_premise = C.Name "USED"
+
+let mk_exp_args hd tl classes synth =
+ let meta id = C.AImplicit (id, None) in
+ let map v (cl, b) =
+ if I.overlaps synth cl && b then v else meta ""
+ in
+ let rec aux = function
+ | [] -> []
+ | hd :: tl -> if hd = meta "" then aux tl else List.rev (hd :: tl)
+ in
+ let args = T.list_rev_map2 map tl classes in
+ let args = aux args in
+ if args = [] then hd else C.AAppl ("", hd :: args)
+
+let mk_convert st ?name sty ety note =
+ let e = Cn.hole "" in
+ let csty, cety = H.cic sty, H.cic ety in
+ let _note = Printf.sprintf "%s\nSINTH: %s\nEXP: %s"
+ note (Pp.ppterm csty) (Pp.ppterm cety)
+ in
+ if Ut.alpha_equivalence csty cety then [(* T.Note note *)] else
+ match name with
+ | None -> [T.Change (sty, ety, None, e, ""(*note*))]
+ | Some (id, i) ->
+ begin match get_entry st id with
+ | C.Def _ -> assert false (* [T.ClearBody (id, note)] *)
+ | C.Decl _ -> [T.Change (ety, sty, Some (id, Some id), e, "" (* note *))]
+ end