Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-17 19:26:38 -0800 (Thu, 17 Feb 2000)
Revision: 2889
Log message:
- When compiling a MetaPRL file referenced using its path instead of
just a name, only the basename is now used as the theory name.
This allowed me to put some MetaPRL files into a separate directory
without having to give them their own Makefile and still be able
to cd the theories produced by those files.
However, that "separate directory" still has to be added to the
include pacth (using the -I command) in order for this to work.
- Added a new mk/config variable TESTS that specifies whether to compile
various test theories (itt_test, test, prop-pigeon) into MetaPRL.
By default it is set to "no".
- Added the prop-pigeon theory and put the pigeon2 - pigeon9 theorems there.
I still have to recover pigeonT from the CVS repository and fix propDecideT
to be able to test these.