(Cic.id, Cic2acic.sort_kind) Hashtbl.t)) (* ids_to_inner_sorts *)
val nmml_of_cic_sequent:
+ #NCicCoercion.status ->
NCic.metasenv -> NCic.substitution -> (* metasenv, substitution *)
int * NCic.conjecture -> (* sequent *)
- Gdome.document * (* Math ML *)
- (string, NTermCicContent.id option) Hashtbl.t (* id -> father id *)
+ Gdome.document (* Math ML *)
val mml_of_cic_object:
Cic.obj -> (* object *)
(Cic.id, Cic2acic.sort_kind) Hashtbl.t * (* ids_to_inner_sorts *)
(Cic.id, Cic2acic.anntypes) Hashtbl.t)) (* ids_to_inner_types *)
-val nmml_of_cic_object:
- NCic.obj -> Gdome.document *
- (string, NTermCicContent.id option) Hashtbl.t (* id -> father id *)
-
+val nmml_of_cic_object: #NCicCoercion.status -> NCic.obj -> Gdome.document
val txt_of_cic_term:
map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.context -> Cic.term ->