]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/binaries/matitaprover/tptp_cnf.ml
better doc
[helm.git] / helm / software / components / binaries / matitaprover / tptp_cnf.ml
index bebce17e7cfeef47d3ed8808d55d6b44ac8c7cf0..ffac7658523f917e298a51b7536a807130f732c7 100644 (file)
@@ -17,12 +17,13 @@ let trans_formulae ~neg = function
 (* HELPERS *)
 let resolve ~tptppath s = 
   let resolved_name = 
-    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 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
   in
   if HExtlib.is_regular resolved_name then
     resolved_name