matitac now compiles like make (recorsively) if needed.

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

diff --git a/components/grafite_engine/grafiteTypes.mli b/components/grafite_engine/grafiteTypes.mli
index a8eb19ac905f9b0c1d5987bc44cec227103b0992..8d9b81ed8dc4e37503f0c6ca0d9d4955c7a437b8 100644 (file)
--- 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