better doc

[helm.git] / helm / software / components / binaries / matitaprover / matitaprover.ml

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