(* *)
(***************************************************************************)
-val mml_of_cic_sequent :
+val mml_of_cic_sequent:
Cic.metasenv -> (* metasenv *)
Cic.conjecture -> (* sequent *)
Gdome.document * (* Math ML *)
(Cic.id, Cic.hypothesis) Hashtbl.t * (* id -> hypothesis *)
(Cic.id, string) Hashtbl.t)) (* ids_to_inner_sorts *)
-val mml_of_cic_object :
- UriManager.uri -> (* object uri *)
- Cic.obj -> (* uri *)
+val mml_of_cic_object:
+ Cic.obj -> (* object *)
Gdome.document * (* Math ML *)
(Cic.annobj * (* annobj *)
((Cic.id, Cic.term) Hashtbl.t * (* id -> term *)