pathname_of_annuri (UriManager.buri_of_uri uri)
in
let list_of_universes =
- CicUnivUtils.universes_of_obj (Cic.Constant ("",None,ty,[]))
+ CicUnivUtils.universes_of_obj uri (Cic.Constant ("",None,ty,[]))
in
let u1_clean = CicUniv.clean_ugraph u1 list_of_universes in
let u2 = CicUniv.fill_empty_nodes_with_uri u1_clean uri in
(`Error (`T (Printexc.to_string e)))
in
let show_in_show_window_uri uri =
- let obj,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+ let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
show_in_show_window_obj uri obj
in
let show_in_show_window_callback mmlwidget ((n : Gdome.element option),_,_,_) =
ignore(CicTypeChecker.typecheck uri CicUniv.empty_ugraph);
(* TASSI: typecheck mette la uri nell'env... cosa fa la open_ ?*)
let metasenv,bo,ty =
- match fst(CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph) with
+ match fst(CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri ) with
Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
| Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty
| Cic.Constant _