Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-06 14:20:48 -0700 (Wed, 06 Aug 2003)
Revision: 4817
Log message:

      Added some support for sequent operations.
      
      subC now works correctly for sequents, but the sequent test is in the
      inner loop, so it will be a little slower.
      
      Haven't changed higherC yet.
      
      Added sequent support in Term_op_ds.{map_up,map_down}.
      

Changes  Path
+5 -0 metaprl/OMakefile
+38 -17 metaprl/editor/ml/shell_mp.ml
+67 -18 metaprl/filter/boot/conversionals_boot.ml
+13 -3 metaprl/filter/boot/exn_boot.ml
+1 -0 metaprl/filter/boot/exn_boot.mli
+8 -8 metaprl/filter/boot/rewrite_boot.ml
+1 -0 metaprl/filter/boot/tactic_boot_sig.mlz
+2 -2 metaprl/refiner/reflib/term_match_table.ml
+1 -0 metaprl/refiner/refsig/term_addr_sig.ml
+5 -2 metaprl/refiner/term_ds/term_addr_ds.ml
+3 -3 metaprl/refiner/term_ds/term_base_ds.ml
+42 -2 metaprl/refiner/term_ds/term_op_ds.ml
+8 -4 metaprl/refiner/term_ds/term_op_ds.mli
+1 -1 metaprl/refiner/term_gen/term_addr_gen.ml
+0 -2 metaprl/support/shell/shell.ml
+5 -6 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_name.ml