* http://cs.unibo.it/helm/.
*)
-exception NotImplemented
exception NotEnoughElements
exception NameExpected
-exception Found of (Cic.name * Cic.context_entry) list
-exception NotImplemented
+
+val source_id_of_id : string -> string
+
+type anntypes =
+ {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option}
+;;
val acic_of_cic_context' :
int ref -> (* seed *)
(Cic.id, Cic.term) Hashtbl.t -> (* ids_to_terms *)
(Cic.id, Cic.id option) Hashtbl.t -> (* ids_to_father_ids *)
(Cic.id, string) Hashtbl.t -> (* ids_to_inner_sorts *)
- (Cic.id, Cic.annterm) Hashtbl.t -> (* ids_to_inner_types *)
+ (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 *)
val acic_object_of_cic_object :
(Cic.id, Cic.term) Hashtbl.t * (* ids_to_terms *)
(Cic.id, Cic.id option) Hashtbl.t * (* ids_to_father_ids *)
(Cic.id, string) Hashtbl.t * (* ids_to_inner_sorts *)
- (Cic.id, Cic.annterm) Hashtbl.t * (* ids_to_inner_types *)
+ (Cic.id, anntypes) Hashtbl.t * (* ids_to_inner_types *)
(Cic.id, Cic.conjecture) Hashtbl.t * (* ids_to_conjectures *)
(Cic.id, Cic.hypothesis) Hashtbl.t (* ids_to_hypotheses *)