* http://cs.unibo.it/helm/.
*)
-exception NotEnoughElements
+exception NotEnoughElements of string
val source_id_of_id : string -> string
{annsynthesized : Cic.annterm ; annexpected : Cic.annterm option}
;;
-type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ]
+type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe | `NType of string | `NCProp of string]
val string_of_sort: sort_kind -> string
(*val sort_of_string: string -> sort_kind*)
(Cic.id, Cic.hypothesis) Hashtbl.t) (* ids_to_hypotheses *)
val plain_acic_object_of_cic_object : Cic.obj -> Cic.annobj
+
+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 *)