Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2001-11-19 07:09:10 -0800 (Mon, 19 Nov 2001)
Revision: 3449
Log message:

      First working version with meta-prl/mc together.
      
      To compile with mc, as of Mon Nov 19 07:04:50 PST 2001:
         0. Get a copy of mc, available from mojave.cs.caltech.edu.
            If you don't know how, you can ask jyh@cs.caltech.edu.
         1. set the MC_ROOT environment variable to the root
            directory for mc.
         2. Compile using cons.  You chould compile from the root
            meta-prl directory first.  After that, you can build
            from the editor/ml directory (use cons -t).
      
      There are still some problems with dependencies in theories/tactic.
      prlc adds a lot of implicit dependencies, and I've only caught a few
      of them.  It compiles for now, but beware of "undefined modules" in
      editor/ml.
      

Changes  Path
+5 -0 metaprl/Conscript
+45 -3 metaprl/editor/ml/Conscript
+1 -1 metaprl/refiner/reflib/Conscript
+4 -0 metaprl/refiner/reflib/jall.ml
+5 -3 metaprl/theories/mc/Conscript
+5 -3 metaprl/theories/tactic/Conscript