+type mml_of_cic_sequent =
+ Cic.metasenv ->
+ int * Cic.context * Cic.term ->
+ Gdome.document *
+ (Cic.annconjecture *
+ ((Cic.id, Cic.term) Hashtbl.t *
+ (Cic.id, Cic.id option) Hashtbl.t *
+ (string, Cic.hypothesis) Hashtbl.t *
+ (Cic.id, string) Hashtbl.t))
+
+
+type mml_of_cic_object =
+ Cic.obj ->
+ Gdome.document *
+ (Cic.annobj *
+ ((Cic.id, Cic.term) Hashtbl.t *
+ (Cic.id, Cic.id option) Hashtbl.t *
+ (Cic.id, Cic.conjecture) Hashtbl.t *
+ (Cic.id, Cic.hypothesis) Hashtbl.t *
+ (Cic.id, string) Hashtbl.t *
+ (Cic.id, Cic2acic.anntypes) Hashtbl.t))
+