X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=24872ffd0c408ceffdb163eb58499baa125946c8;hb=e6b28085c97ae7b9bd3f3262b105f6b84f42b047;hp=da3a730fb7831212b17c5f6ab09b012fefe78e2a;hpb=6d93d688ae2da401417f64ffd5ee6ffccaa89fc1;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index da3a730fb..24872ffd0 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -126,7 +126,7 @@ let tactic_of_ast = function
       | `Normalize -> Tactics.normalize ~pattern
       | `Reduce -> Tactics.reduce ~pattern  
       | `Simpl -> Tactics.simpl ~pattern 
-      | `Unfold what -> Tactics.unfold ~pattern ?what
+      | `Unfold what -> Tactics.unfold ~pattern what
       | `Whd -> Tactics.whd ~pattern)
   | GrafiteAst.Reflexivity _ -> Tactics.reflexivity
   | GrafiteAst.Replace (_, pattern, with_what) ->
@@ -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 =