...

diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml
index 499ecb2738343e127c1f12709a4a214955408d4f..92de3c4c5489c8d00de94b1204d5ce53c0078fd8 100644 (file)
--- a/helm/software/components/binaries/matitaprover/matitaprover.ml
+++ b/helm/software/components/binaries/matitaprover/matitaprover.ml
@@ -56,6 +56,12 @@ Matita interactive theorem prover (http://matita.cs.unibo.it).
 
 Developed by A.Asperti, M.Denes and E.Tassi, released under GPL-2.1
 
+If --tptppath is given, instead of the problem file you can just give the 
+problem name with the .p suffix (e.g. BOO001-1.p)
+
+If --tptppath is not given, included files (i.e. axiom sets) are searched 
+in the current directory only.
+
 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