new cicEnvironment implementation

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 2276fdac4055c33d612a0a95fc3376a347f55c4a..e06c02297454c3e532fe877c083d9301cb6afccd 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -460,7 +460,7 @@ let qed () =
                    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
@@ -880,7 +880,7 @@ let
        (`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),_,_,_) =
@@ -1593,7 +1593,7 @@ let open_ () =
      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 _