better doc

diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml
index 2a5f9fdb069da24746b75e370b4e3aeaea0de5d0..499ecb2738343e127c1f12709a4a214955408d4f 100644 (file)
--- a/helm/software/components/binaries/matitaprover/matitaprover.ml
+++ b/helm/software/components/binaries/matitaprover/matitaprover.ml
@@ -31,7 +31,7 @@ hash "==";;
 hash "_";;
 
 let problem_file = ref "no-file-given";;
-let tptppath = ref "./";;
+let tptppath = ref "/";;
 let seconds = ref 300;;
 
 let fail_msg () =
@@ -50,10 +50,17 @@ let main () =
      ("[path]  TPTP lib root, default " ^ !tptppath);
    "--timeout", Arg.Int (fun p -> seconds := p), 
      ("[seconds]  timeout, default " ^ string_of_int !seconds);
-   ] (fun x -> problem_file := x) "matitaprover [problemfile]";
+   ] (fun x -> problem_file := x) "
+Matitaprover is the first order automatic prover that equips the 
+Matita interactive theorem prover (http://matita.cs.unibo.it).
+
+Developed by A.Asperti, M.Denes and E.Tassi, released under GPL-2.1
+
+usage: matitaprover [options] problemfile";
   let hypotheses, goals = Tptp_cnf.parse ~tptppath:!tptppath !problem_file in
   let goal = match goals with [x] -> x | _ -> assert false in
-  let module B : Terms.Blob with type t = leaf and type input = Ast.term = struct
+  let module B : Terms.Blob 
+  with type t = leaf and type input = Ast.term = struct
         type t = leaf
         let eq a b = a == b
         let compare (a,_) (b,_) = Pervasives.compare a b

diff --git a/helm/software/components/binaries/matitaprover/tptp_cnf.ml b/helm/software/components/binaries/matitaprover/tptp_cnf.ml
index bebce17e7cfeef47d3ed8808d55d6b44ac8c7cf0..ffac7658523f917e298a51b7536a807130f732c7 100644 (file)
--- a/helm/software/components/binaries/matitaprover/tptp_cnf.ml
+++ b/helm/software/components/binaries/matitaprover/tptp_cnf.ml
@@ -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

diff --git a/helm/software/components/binaries/matitaprover/tptp_cnf.mli b/helm/software/components/binaries/matitaprover/tptp_cnf.mli
index 9e56414d454ba6b710ea8c1f74c4090c14fcc67f..48b57dbd7964a463cd74546c9a8a29a8e92d7de7 100644 (file)
--- a/helm/software/components/binaries/matitaprover/tptp_cnf.mli
+++ b/helm/software/components/binaries/matitaprover/tptp_cnf.mli
@@ -1,3 +1,16 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.      
+     \ /   This software is distributed as is, NO WARRANTY.     
+      V_______________________________________________________________ *)
+
+(* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
+
 val parse: 
       tptppath:string -> string -> 
          (Ast.term * Ast.term) list * (Ast.term * Ast.term) list