]> matita.cs.unibo.it Git - helm.git/commitdiff
...
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 1 Jul 2009 16:07:16 +0000 (16:07 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 1 Jul 2009 16:07:16 +0000 (16:07 +0000)
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