type mml_of_cic_object =
- UriManager.uri ->
Cic.obj ->
Gdome.document *
(Cic.annobj *
end
| None -> assert false (* "ERROR: No selection!!!" *)
- method load_proof uri currentproof =
+ method load_proof currentproof =
let mml,
(acic,
(ids_to_terms,ids_to_father_ids,ids_to_conjectures,
ids_to_hypotheses,ids_to_inner_sorts,ids_to_inner_types)) =
- mml_of_cic_object uri currentproof
+ mml_of_cic_object currentproof
in
current_infos <-
Some