X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaEngine.ml;h=cd5c8344198288c08dbfd1cd471686fc1c6fad42;hb=c881200303035c81106f09c4fafb06119a38c157;hp=1efaeff24834ce7b09cdbd3f1eb619d0ece0a270;hpb=d6eeb40f4796a582934c3d0b6a4dd5ae6f3b768f;p=helm.git

diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml
index 1efaeff24..cd5c83441 100644
--- a/matita/matita/matitaEngine.ml
+++ b/matita/matita/matitaEngine.ml
@@ -288,7 +288,7 @@ and compile ~compiling ~include_paths fname =
 (* BIG BUG: if a file recursively includes itself, anything can happen,
  * from divergence to inclusion of an old copy of itself *)
 and assert_ng ~compiling ~include_paths ~root mapath =
- let root',baseuri,_,_ = Librarian.baseuri_of_script ~include_paths mapath in
+ let root',baseuri,fullmapath,_ = Librarian.baseuri_of_script ~include_paths mapath in
  assert (root=root');
  let baseuri = NUri.uri_of_string baseuri in
  let ngpath = NCicLibrary.ng_path_of_baseuri baseuri in
@@ -297,8 +297,8 @@ and assert_ng ~compiling ~include_paths ~root mapath =
    Some (Unix.stat ngpath).Unix.st_mtime
   with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = ngpath -> None in
  let matime =
-  try (Unix.stat mapath).Unix.st_mtime
-  with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = mapath -> assert false
+  try (Unix.stat fullmapath).Unix.st_mtime
+  with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = fullmapath -> assert false
  in
  let to_be_compiled =
   match ngtime with
@@ -317,7 +317,7 @@ and assert_ng ~compiling ~include_paths ~root mapath =
      (* maybe recompiling it I would get the same... *)
      raise (AlreadyLoaded (lazy mapath))
    else
-    (compile ~compiling ~include_paths mapath; true)
+    (compile ~compiling ~include_paths fullmapath; true)
 ;;
 
 let assert_ng = assert_ng ~compiling:[]