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 *)
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, anntypes) Hashtbl.t -> (* ids_to_inner_types *)
Cic.metasenv -> (* metasenv *)
Cic.context -> (* context *)
(Cic.id, anntypes) Hashtbl.t -> (* ids_to_inner_types *)
Cic.metasenv -> (* metasenv *)
Cic.context -> (* context *)
Cic.obj -> (* object *)
Cic.annobj * (* annotated object *)
(Cic.id, Cic.term) Hashtbl.t * (* ids_to_terms *)
(Cic.id, Cic.id option) Hashtbl.t * (* ids_to_father_ids *)
Cic.obj -> (* object *)
Cic.annobj * (* annotated object *)
(Cic.id, Cic.term) Hashtbl.t * (* ids_to_terms *)
(Cic.id, Cic.id option) Hashtbl.t * (* ids_to_father_ids *)
(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 *)
(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 *)
Cic.annconjecture * (* annotated conjecture *)
(Cic.id, Cic.term) Hashtbl.t * (* ids_to_terms *)
(Cic.id, Cic.id option) Hashtbl.t * (* ids_to_father_ids *)
Cic.annconjecture * (* annotated conjecture *)
(Cic.id, Cic.term) Hashtbl.t * (* ids_to_terms *)
(Cic.id, Cic.id option) Hashtbl.t * (* ids_to_father_ids *)