X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Flibrary%2Flibrarian.ml;fp=matita%2Fcomponents%2Flibrary%2Flibrarian.ml;h=791141b88c23f4233f51f4b990ac543b07f49348;hb=2e72565d67fee9207f4b08448a71d7b3ef815c20;hp=7d159af2467a26cddfac6ef9e4863a42961db0d4;hpb=4e7e01cd771c07b3605ba54d3853ac34a02cb86d;p=helm.git

diff --git a/matita/components/library/librarian.ml b/matita/components/library/librarian.ml
index 7d159af24..791141b88 100644
--- a/matita/components/library/librarian.ml
+++ b/matita/components/library/librarian.ml
@@ -80,17 +80,10 @@ let find_root_for ~include_paths file =
    let rec find_path_for file =
       try HExtlib.find_in include_paths file
       with Failure "find_in" -> 
-         if Filename.check_suffix file ".ma" then begin
-            let mma = Filename.chop_suffix file ".ma" ^ ".mma" in
-            HLog.warn ("We look for: " ^ mma);
-            let path = find_path_for mma in
-	    Filename.chop_suffix path ".mma" ^ ".ma"
-         end else begin
-            HLog.error ("We are in: " ^ Sys.getcwd ());
-            HLog.error ("Unable to find: "^file^"\nPaths explored:");
-            List.iter (fun x -> HLog.error (" - "^x)) include_paths;
-            raise (NoRootFor file)
-         end         
+       HLog.error ("We are in: " ^ Sys.getcwd ());
+       HLog.error ("Unable to find: "^file^"\nPaths explored:");
+       List.iter (fun x -> HLog.error (" - "^x)) include_paths;
+       raise (NoRootFor file)
    in
    let path = find_path_for file in   
    let path = absolutize path in