matitac now compiles like make (recorsively) if needed.

[helm.git] / components / grafite_engine / grafiteTypes.ml

diff --git a/components/grafite_engine/grafiteTypes.ml b/components/grafite_engine/grafiteTypes.ml
index 01fb19c5846b9662e0193ddb371c41851a6850c1..af819555bec8cac3bdd4f246c50a5948068bdcc2 100644 (file)
--- 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