(Cic.id, Cic.hypothesis) Hashtbl.t * (* id -> hypothesis *)
(Cic.id, Cic2acic.sort_kind) Hashtbl.t)) (* ids_to_inner_sorts *)
+val nmml_of_cic_sequent:
+ NCic.metasenv -> NCic.substitution -> (* metasenv, substitution *)
+ int * NCic.conjecture -> (* sequent *)
+ Gdome.document (* Math ML *)
+
val mml_of_cic_object:
Cic.obj -> (* object *)
Gdome.document * (* Math ML *)