type mml_of_cic_object =
- UriManager.uri ->
Cic.obj ->
Gdome.document *
(Cic.annobj *
(* load_proof also returns the annotated cic term and the *)
(* ids_to_inner_types and ids_to_inner_sorts maps. *)
method load_proof :
- UriManager.uri -> Cic.obj ->
+ Cic.obj ->
Cic.annobj * (Cic.id, Cic2acic.anntypes) Hashtbl.t *
(Cic.id, string) Hashtbl.t