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

diff --git a/components/grafite_engine/grafiteTypes.mli b/components/grafite_engine/grafiteTypes.mli
index a8eb19ac9..8d9b81ed8 100644
--- a/components/grafite_engine/grafiteTypes.mli
+++ b/components/grafite_engine/grafiteTypes.mli
@@ -55,7 +55,7 @@ type status = {
   objects: UriManager.uri list;  (** in-scope objects *)
   coercions: UriManager.uri list; (** defined coercions *)
   universe:Universe.universe;  (** universe of terms used by auto *)
-  baseuri: string option;
+  baseuri: string;
 }
 
 val dump_status : status -> unit
@@ -66,8 +66,7 @@ val add_moo_content: GrafiteMarshal.ast_command list -> status -> status
 val get_option : status -> string -> option_value
 val get_string_option : status -> string -> string
 val set_option : status -> string -> string -> status
-(* to cache the baseuri of current file *)
-val get_baseuri: status -> string * status
+val get_baseuri: status -> string 
 
 val get_current_proof: status -> ProofEngineTypes.proof
 val get_proof_metasenv: status ->  Cic.metasenv