]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/binaries/matitaprover/tptp_cnf.ml
...
[helm.git] / helm / software / components / binaries / matitaprover / tptp_cnf.ml
index 8c38d6e6571eaee3b27064fc867a57c4a257d93c..8d3cedfd4f9e90ad05f3e976f1099d788e634bc8 100644 (file)
@@ -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