]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/library/librarian.ml
Most warnings turned into errors and avoided
[helm.git] / matita / components / library / librarian.ml
index 9ffde2b87d0444c6d9ad012b4e26e9641d45a513..bcb84fd6791f9f142defb474dd33f6c8c83958cd 100644 (file)
@@ -41,7 +41,7 @@ let find_root path =
   let path = absolutize path in
   let paths = List.rev (Str.split (Str.regexp "/") path) in
   let rec build = function
-    | he::tl as l -> ("/" ^ String.concat "/" (List.rev l) ^ "/") :: build tl
+    | _he::tl as l -> ("/" ^ String.concat "/" (List.rev l) ^ "/") :: build tl
     | [] -> ["/"]
   in
   let paths = List.map HExtlib.normalize_path (build paths) in
@@ -78,7 +78,7 @@ let load_root_file rootpath =
 
 let find_root_for ~include_paths file = 
   let include_paths = "" :: Sys.getcwd () :: include_paths in
-   let rec find_path_for file =
+   let find_path_for file =
       try HExtlib.find_in include_paths file
       with Failure "find_in" -> 
        HLog.error ("We are in: " ^ Sys.getcwd ());
@@ -111,8 +111,12 @@ let find_root_for ~include_paths file =
 
 let mk_baseuri root extra =
   let chop name = 
+(* FG: there is no reason why matita should edit just matita files
+       matita's editor is good on its own and has interesting facilities
+       including predefined virtuals
     assert(Filename.check_suffix name ".ma" ||
       Filename.check_suffix name ".mma");
+*)    
     try Filename.chop_extension name
     with Invalid_argument "Filename.chop_extension" -> name
   in