+ (fun context t ->
+ let map = function
+ | None -> None
+ | Some (n, C.Decl ty) -> Some (n, C.Decl (Unshare.unshare ty))
+ | Some (n, C.Def (bo, ty)) ->
+ Some (n, C.Def (Unshare.unshare bo, Unshare.unshare ty))
+ in
+ let t = Unshare.unshare t in
+ let context = List.map map context in
+ let idrefs = List.map (function _ -> gen_id seed) context in
+ let t = acic_term_of_cic_term_context' ~computeinnertypes:true [] context idrefs t None in
+ t, ids_to_inner_sorts, ids_to_inner_types
+ ),(function obj ->