Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-19 14:40:52 -0800 (Wed, 19 Jan 2005)
Revision: 6445
Log message:

      Make it easier to mix MetaPRL and non-MetaPRL .ml files in theories.
      
      This is useful because non-MetaPRL compilation makes .mli optional,
      is faster, iand can be done without waiting for the filter to be built.
      

Changes	Path
+34 -25	metaprl/OMakefile
+0 -5	metaprl/OMakeroot
+5 -4	metaprl/editor/ml/OMakefile
+1 -0	metaprl/editor/ml/tests/OMakefile
Deleted	metaprl/support/shell/Files
+59 -2	metaprl/support/shell/OMakefile
+0 -4	metaprl/support/shell/shell.ml
+0 -3	metaprl/support/shell/shell.mli
+0 -2	metaprl/support/shell/shell_fs.ml
+0 -3	metaprl/support/shell/shell_package.ml
+0 -2	metaprl/support/shell/shell_root.ml
+0 -1	metaprl/support/shell/shell_theory.mlz
+1 -1	metaprl/support/tactics/OMakefile
+0 -0	metaprl/theories/itt/itt_rbtree.mli