X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_engine%2FgrafiteTypes.ml;h=af819555bec8cac3bdd4f246c50a5948068bdcc2;hb=5356519d50425dfca5b42ad5faeb2181d4240c78;hp=01fb19c5846b9662e0193ddb371c41851a6850c1;hpb=35a06fa8d6c2664301b59e77dcbff5bcfd4a5091;p=helm.git

diff --git a/components/grafite_engine/grafiteTypes.ml b/components/grafite_engine/grafiteTypes.ml
index 01fb19c58..af819555b 100644
--- a/components/grafite_engine/grafiteTypes.ml
+++ b/components/grafite_engine/grafiteTypes.ml
@@ -58,7 +58,7 @@ type status = {
   objects: UriManager.uri list;
   coercions: UriManager.uri list;
   universe:Universe.universe;  
-  baseuri: string option;
+  baseuri: string;
 }
 
 let get_current_proof status =
@@ -142,13 +142,7 @@ let get_option status name =
     StringMap.find name status.options
   with Not_found -> raise (Option_error (name, "not found"))
  
-let get_baseuri status =
-  match status.baseuri with
-  | Some b -> b, status
-  | None -> 
-      let _,baseuri,_ = Librarian.baseuri_of_script (Librarian.filename()) in
-      baseuri, {status with baseuri = Some baseuri}
-;;
+let get_baseuri status = status.baseuri;;
 
 let set_option status name value =
   let types = [ (* no set options defined! *) ] in