From 65e1aa022da79a3a880f5c2d5d0d512b80e50635 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 25 Jun 2009 21:29:22 +0000 Subject: [PATCH] ... --- .../components/binaries/matitaprover/matitaprover.ml | 6 ++++++ 1 file changed, 6 insertions(+) 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 -- 2.39.2