0. core_notation.ma splitted into coq.moo and core_notation.moo

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index f329780633b423d2d0d626fdfd6ad18cb4b34156..24872ffd0c408ceffdb163eb58499baa125946c8 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -518,17 +518,19 @@ let disambiguate_command status = function
        status, GrafiteAst.Obj (loc,obj)
 
 let make_absolute paths path =
-  let rec aux = function
-  | [] -> ignore (Unix.stat path); path
-  | p :: tl ->
-     let path = p ^ "/" ^ path in
-      try
-        ignore (Unix.stat path); path
-      with Unix.Unix_error _ -> aux tl
-  in
-  try
-    aux paths
-  with Unix.Unix_error _ as exc -> raise (UnableToInclude path)
+  if path = "coq.ma" then path
+  else
+   let rec aux = function
+   | [] -> ignore (Unix.stat path); path
+   | p :: tl ->
+      let path = p ^ "/" ^ path in
+       try
+         ignore (Unix.stat path); path
+       with Unix.Unix_error _ -> aux tl
+   in
+   try
+     aux paths
+   with Unix.Unix_error _ as exc -> raise (UnableToInclude path)
 ;;
        
 let eval_command opts status cmd =