* http://cs.unibo.it/helm/.
*)
-exception NotImplemented
exception NotEnoughElements
exception NameExpected
+val source_id_of_id : string -> string
+
type anntypes =
{annsynthesized : Cic.annterm ; annexpected : Cic.annterm option}
;;
(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 *)