Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-11 14:31:31 -0700 (Mon, 11 Aug 2003)
Revision: 4821
Log message:

      . Fixed several things to work with sequents.
      .    1. In apply_redex, return *something* for a StackSeqContext.
      .       Even though we can't return the right thing, this should
      .       not fail.
      .    2. term_match_table now works with sequents.
      .
      . It is possible to define display form for sequents the normal way.
      . See core_ast.ml for an example.
      .
      . In core, the namer now works, type inference is stuck because
      . Unify_mm needs to be upgraded to work with sequents.
      

Changes  Path
+0 -5 metaprl/OMakefile
+10 -10 metaprl/editor/ml/shell_mp.ml
+8 -8 metaprl/filter/boot/conversionals_boot.ml
+9 -0 metaprl/mk/make_config.sh
+1 -1 metaprl/refiner/reflib/dform.ml
+389 -133 metaprl/refiner/reflib/term_match_table.ml
+2 -0 metaprl/refiner/reflib/term_match_table.mli
+3 -1 metaprl/refiner/refsig/term_shape_sig.ml
+5 -1 metaprl/refiner/rewrite/rewrite.ml
+3 -3 metaprl/refiner/rewrite/rewrite_debug.ml
+5 -5 metaprl/refiner/rewrite/rewrite_debug.mli
+1 -0 metaprl/refiner/rewrite/rewrite_debug_sig.ml
+2 -2 metaprl/refiner/term_ds/term_addr_ds.ml
+47 -16 metaprl/refiner/term_gen/term_shape_gen.ml
+3 -3 metaprl/support/display/base_dform.ml
+5 -0 metaprl/support/shell/shell.ml
+5 -0 metaprl/support/shell/shell.mli
+1 -1 metaprl/util/check-status.sh
+1 -0 mpcompiler-branches/mojave_sequents/mmc/core/Files
+2 -2 mpcompiler-branches/mojave_sequents/mmc/core/core_test.ml
+11 -22 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_ast.ml
+1 -2 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_ast.mli
Added mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_ast_util.ml
Properties mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_ast_util.ml
Added mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_ast_util.mli
Properties mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_ast_util.mli
+17 -7 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_name.ml
+8 -2 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_name.mli
+58 -10 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_type_infer.ml