From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 25 Jun 2009 21:29:22 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~3789
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=65e1aa022da79a3a880f5c2d5d0d512b80e50635;p=helm.git

...
---

diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml
index 499ecb273..92de3c4c5 100644
--- 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