Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-28 21:41:30 -0700 (Mon, 28 Jul 2003)
Revision: 4783
Log message:

      Merged the bound_contexts branch with the latest trunk changes and re-branched.
      

Changes  Path
+3 -3 metaprl-branches/bound_contexts2/Makefile
+8 -4 metaprl-branches/bound_contexts2/filter/base/filter_magic.ml
+8 -28 metaprl-branches/bound_contexts2/filter/base/filter_summary.ml
+3 -3 metaprl-branches/bound_contexts2/filter/base/filter_summary_util.ml
+21 -1 metaprl-branches/bound_contexts2/filter/base/filter_type.ml
+6 -1 metaprl-branches/bound_contexts2/filter/base/filter_util.ml
+2 -0 metaprl-branches/bound_contexts2/filter/base/filter_util.mli
+0 -2 metaprl-branches/bound_contexts2/filter/boot/sequent_boot.ml
+0 -1 metaprl-branches/bound_contexts2/filter/boot/tactic_boot_sig.mlz
+42 -16 metaprl-branches/bound_contexts2/filter/filter/filter_parse.ml
+4 -5 metaprl-branches/bound_contexts2/filter/filter/filter_patt.ml
+39 -42 metaprl-branches/bound_contexts2/filter/filter/term_grammar.ml
+1 -17 metaprl-branches/bound_contexts2/filter/filter/term_grammar.mli
+3 -1 metaprl-branches/bound_contexts2/filter/phobos/phobos_parser.mly
+6 -5 metaprl-branches/bound_contexts2/refiner/refiner/refine.ml
+1 -1 metaprl-branches/bound_contexts2/refiner/refiner/refine_error.ml
+4 -3 metaprl-branches/bound_contexts2/refiner/refiner/refiner_ds.ml
+4 -3 metaprl-branches/bound_contexts2/refiner/refiner/refiner_std.ml
+2 -2 metaprl-branches/bound_contexts2/refiner/reflib/Files
+1 -1 metaprl-branches/bound_contexts2/refiner/reflib/arith.ml
+93 -19 metaprl-branches/bound_contexts2/refiner/reflib/ascii_io.ml
+6 -4 metaprl-branches/bound_contexts2/refiner/reflib/ascii_io_sig.ml
+20 -13 metaprl-branches/bound_contexts2/refiner/reflib/dform.ml
+45 -47 metaprl-branches/bound_contexts2/refiner/reflib/jall.ml
+1 -1 metaprl-branches/bound_contexts2/refiner/reflib/match_seq.ml
+10 -4 metaprl-branches/bound_contexts2/refiner/reflib/refine_exn.ml
+47 -52 metaprl-branches/bound_contexts2/refiner/reflib/simple_print.ml
+3 -3 metaprl-branches/bound_contexts2/refiner/reflib/term_compare.ml
+1 -1 metaprl-branches/bound_contexts2/refiner/reflib/term_match_table.ml
+1 -1 metaprl-branches/bound_contexts2/refiner/refsig/refine_error_sig.ml
+1 -0 metaprl-branches/bound_contexts2/refiner/refsig/term_addr_sig.ml
+43 -48 metaprl-branches/bound_contexts2/refiner/refsig/term_base_minimal_sig.ml
+6 -10 metaprl-branches/bound_contexts2/refiner/refsig/term_base_sig.ml
+3 -1 metaprl-branches/bound_contexts2/refiner/refsig/term_hash_sig.ml
+4 -0 metaprl-branches/bound_contexts2/refiner/refsig/term_man_minimal_sig.ml
+12 -1 metaprl-branches/bound_contexts2/refiner/refsig/term_man_sig.ml
+10 -0 metaprl-branches/bound_contexts2/refiner/refsig/term_meta_sig.ml
+1 -1 metaprl-branches/bound_contexts2/refiner/refsig/term_sig.ml
+1 -33 metaprl-branches/bound_contexts2/refiner/refsig/termmod_hash_sig.ml
+6 -0 metaprl-branches/bound_contexts2/refiner/refsig/termmod_sig.ml
+6 -5 metaprl-branches/bound_contexts2/refiner/rewrite/rewrite.ml
+2 -2 metaprl-branches/bound_contexts2/refiner/rewrite/rewrite_build_contractum.ml
+53 -44 metaprl-branches/bound_contexts2/refiner/rewrite/rewrite_compile_contractum.ml
+95 -78 metaprl-branches/bound_contexts2/refiner/rewrite/rewrite_compile_redex.ml
+11 -9 metaprl-branches/bound_contexts2/refiner/rewrite/rewrite_debug.ml
+43 -27 metaprl-branches/bound_contexts2/refiner/rewrite/rewrite_match_redex.ml
+4 -4 metaprl-branches/bound_contexts2/refiner/rewrite/rewrite_types.ml
+24 -20 metaprl-branches/bound_contexts2/refiner/rewrite/rewrite_util.ml
+2 -2 metaprl-branches/bound_contexts2/refiner/rewrite/rewrite_util_sig.ml
+1 -1 metaprl-branches/bound_contexts2/refiner/term_ds/Files
+175 -64 metaprl-branches/bound_contexts2/refiner/term_ds/term_addr_ds.ml
+7 -1 metaprl-branches/bound_contexts2/refiner/term_ds/term_addr_ds.mli
+108 -120 metaprl-branches/bound_contexts2/refiner/term_ds/term_base_ds.ml
+2 -1 metaprl-branches/bound_contexts2/refiner/term_ds/term_ds.ml
+13 -8 metaprl-branches/bound_contexts2/refiner/term_ds/term_ds_sig.ml
+77 -65 metaprl-branches/bound_contexts2/refiner/term_ds/term_man_ds.ml
+199 -220 metaprl-branches/bound_contexts2/refiner/term_ds/term_op_ds.ml
+89 -83 metaprl-branches/bound_contexts2/refiner/term_ds/term_subst_ds.ml
+35 -12 metaprl-branches/bound_contexts2/refiner/term_gen/term_addr_gen.ml
+3 -0 metaprl-branches/bound_contexts2/refiner/term_gen/term_addr_gen.mli
+19 -9 metaprl-branches/bound_contexts2/refiner/term_gen/term_hash.ml
+7 -2 metaprl-branches/bound_contexts2/refiner/term_gen/term_header_constr.ml
+134 -35 metaprl-branches/bound_contexts2/refiner/term_gen/term_man_gen.ml
+166 -1 metaprl-branches/bound_contexts2/refiner/term_gen/term_meta_gen.ml
+12 -1 metaprl-branches/bound_contexts2/refiner/term_gen/term_meta_gen.mli
+31 -7 metaprl-branches/bound_contexts2/refiner/term_gen/term_shape_gen.ml
+6 -4 metaprl-branches/bound_contexts2/refiner/term_gen/term_shape_gen.mli
+3 -68 metaprl-branches/bound_contexts2/refiner/term_std/term_base_std.ml
+1 -1 metaprl-branches/bound_contexts2/refiner/term_std/term_std.ml
+2 -7 metaprl-branches/bound_contexts2/refiner/term_std/term_std_sig.ml
+38 -26 metaprl-branches/bound_contexts2/support/display/base_dform.ml
+47 -43 metaprl-branches/bound_contexts2/support/shell/shell.ml
+8 -19 metaprl-branches/bound_contexts2/support/shell/shell_package.ml
+5 -1 metaprl-branches/bound_contexts2/support/shell/shell_rewrite.ml
+8 -19 metaprl-branches/bound_contexts2/support/shell/shell_root.ml
+4 -0 metaprl-branches/bound_contexts2/support/shell/shell_rule.ml
+1 -0 metaprl-branches/bound_contexts2/support/shell/shell_sig.mlz
+33 -9 metaprl-branches/bound_contexts2/support/shell/shell_state.ml
+3 -3 metaprl-branches/bound_contexts2/support/shell/shell_state.mli
+0 -22 metaprl-branches/bound_contexts2/support/tactics/dtactic.ml
+1 -1 metaprl-branches/bound_contexts2/support/tactics/tactic_cache.ml
+1 -1 metaprl-branches/bound_contexts2/support/tactics/top_tacticals.ml
+2 -2 metaprl-branches/bound_contexts2/support/tactics/typeinf.ml
+1 -1 metaprl-branches/bound_contexts2/theories/fir/mfir_tr_exp.ml
+4 -4 metaprl-branches/bound_contexts2/theories/itt/itt_equal.ml
+8 -8 metaprl-branches/bound_contexts2/theories/itt/itt_squash.ml
+3 -3 metaprl-branches/bound_contexts2/theories/itt/itt_struct.ml
+2 -2 metaprl-branches/bound_contexts2/theories/itt/itt_struct.mli
+2 -2 metaprl-branches/bound_contexts2/theories/itt/itt_struct2.ml
+1 -1 metaprl-branches/bound_contexts2/util/check-status