matita now includes compiling. if the file is not compiled it compiles it,

[helm.git] / components / library / librarian.mli

diff --git a/components/library/librarian.mli b/components/library/librarian.mli
index 839d8daa1e80381b3aba4faed09bee8a520cf471..1c305c2654bf49ee0d338f0710760f909d58afd8 100644 (file)
--- a/components/library/librarian.mli
+++ b/components/library/librarian.mli
@@ -2,7 +2,9 @@ exception NoRootFor of string
 
 val find_root: string -> string
 
-(* val parse_root: string -> (string*string) list *)
+val load_root_file: string -> (string*string) list
+
+val absolutize: string -> string 
 
 (* baseuri_of_script ?(inc:REG[matita.includes]) fname 
  *   ->