+
+val acic_term_of_cic_term :
+ ?eta_fix: bool -> (* perform eta_fixing; default: true*)
+ Cic.context -> Cic.term -> (* term and context *)
+ Cic.annterm * (* annotated term *)
+ (Cic.id, sort_kind) Hashtbl.t * (* ids_to_inner_sorts *)
+ (Cic.id, anntypes) Hashtbl.t (* ids_to_inner_types *)