* http://cs.unibo.it/helm/.
*)
-exception NotImplemented
exception NotEnoughElements
exception NameExpected
(Cic.id, anntypes) Hashtbl.t -> (* ids_to_inner_types *)
Cic.metasenv -> (* metasenv *)
Cic.context -> (* context *)
+ Cic.id list -> (* idrefs *)
Cic.term -> (* term *)
Cic.term option -> (* expected type *)
Cic.annterm (* annotated term *)