From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 1 Jul 2009 16:07:16 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~3760
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=54d7e03f1cf38103583b4a30f0f13256d54ad65e;p=helm.git

...
---

diff --git a/helm/software/components/binaries/matitaprover/tptp_cnf.ml b/helm/software/components/binaries/matitaprover/tptp_cnf.ml
index 8c38d6e65..8d3cedfd4 100644
--- a/helm/software/components/binaries/matitaprover/tptp_cnf.ml
+++ b/helm/software/components/binaries/matitaprover/tptp_cnf.ml
@@ -15,13 +15,13 @@ let trans_formulae = function
 (* HELPERS *)
 let resolve ~tptppath s = 
   let resolved_name = 
+    if HExtlib.is_regular s then s else
     if tptppath = "/" then s else
-      if Filename.check_suffix s ".p" then
-        (assert (String.length s > 5);
-        let prefix = String.sub s 0 3 in
-        tptppath ^ "/Problems/" ^ prefix ^ "/" ^ s)
-      else
-        tptppath ^ "/" ^ s
+    if Filename.check_suffix s ".p" then
+     (assert (String.length s > 5);
+     let prefix = String.sub s 0 3 in
+     tptppath ^ "/Problems/" ^ prefix ^ "/" ^ s)
+    else tptppath ^ "/" ^ s
   in
   if HExtlib.is_regular resolved_name then
     resolved_name