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.
      

Changes  Path
+1 -1 metaprl/Makefile
+9 -4 metaprl/editor/ml/Makefile
+1 -1 metaprl/editor/ml/mpconfig
Added metaprl/editor/ml/tests/prop-pigeon.ml
Properties metaprl/editor/ml/tests/prop-pigeon.ml
Added metaprl/editor/ml/tests/prop-pigeon.mli
Properties metaprl/editor/ml/tests/prop-pigeon.mli
+1 -1 metaprl/filter/filter/filter_bin.ml
+1 -1 metaprl/filter/filter/filter_parse.ml
+4 -0 metaprl/mk/make_config.sh
+21 -0 metaprl/mk/preface
+4 -1 metaprl/theories/itt/Makefile