Most warnings turned into errors and avoided

[helm.git] / matita / matita / matitaEngine.ml

diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml
index 5b9b070bcc105f97ebe98a4be377b937df81ed0c..2963e71c45e2cf5c8f4312b9a7c58d48f9ada72e 100644 (file)
--- a/matita/matita/matitaEngine.ml
+++ b/matita/matita/matitaEngine.ml
@@ -25,8 +25,6 @@
 
 (* $Id$ *)
 
-module G = GrafiteAst
-open GrafiteTypes
 open Printf
 
 class status baseuri =
@@ -163,7 +161,7 @@ let baseuri_of_script ~include_paths fname =
 
 (* given a path to a ma file inside the include_paths, returns the
    new include_paths associated to that file *)
-let read_include_paths ~include_paths file =
+let read_include_paths ~include_paths:_ file =
  try 
    let root, _buri, _fname, _tgt = 
      Librarian.baseuri_of_script ~include_paths:[] file in 
@@ -360,10 +358,13 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths mapath =
         let preamble = GrafiteTypes.Serializer.dependencies_of baseuri in
         let asserted,children_bad =
          List.fold_left
-          (fun (asserted,b) mapath ->
-            let asserted,b1 =
-              assert_ng ~already_included ~compiling ~asserted ~include_paths
-               mapath
+          (fun (asserted,b) mapath -> 
+           let asserted,b1 =
+              try 
+              assert_ng ~already_included ~compiling ~asserted ~include_paths
+                mapath
+             with Librarian.NoRootFor _ | Librarian.FileNotFound _ ->
+               asserted, true 
             in
              asserted, b || b1
               || let _,baseuri,_,_ =