Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-31 21:16:57 -0800 (Mon, 31 Jan 2005)
Revision: 6548
Log message:

      Merged the opname_classes2 branch with the trunk changes.
      

Changes  Path
+54 -52 metaprl-branches/opname_classes3/editor/ml/nuprl_eval.ml
+3 -1 metaprl-branches/opname_classes3/editor/ml/nuprl_jprover.ml
+691 -153 metaprl-branches/opname_classes3/filter/base/filter_cache_fun.ml
+1 -0 metaprl-branches/opname_classes3/filter/base/filter_cache_fun.mli
+73 -35 metaprl-branches/opname_classes3/filter/base/filter_exn.ml
+3 -2 metaprl-branches/opname_classes3/filter/base/filter_exn.mli
+41 -0 metaprl-branches/opname_classes3/filter/base/filter_grammar.ml
+7 -0 metaprl-branches/opname_classes3/filter/base/filter_grammar.mli
+7 -4 metaprl-branches/opname_classes3/filter/base/filter_magic.ml
+464 -49 metaprl-branches/opname_classes3/filter/base/filter_summary.ml
+13 -3 metaprl-branches/opname_classes3/filter/base/filter_summary_type.ml
+92 -22 metaprl-branches/opname_classes3/filter/base/filter_type.ml
+7 -11 metaprl-branches/opname_classes3/filter/base/filter_util.ml
+0 -2 metaprl-branches/opname_classes3/filter/base/filter_util.mli
+760 -421 metaprl-branches/opname_classes3/filter/filter/filter_parse.ml
+11 -6 metaprl-branches/opname_classes3/filter/filter/filter_patt.ml
+39 -9 metaprl-branches/opname_classes3/filter/filter/filter_prog.ml
+515 -142 metaprl-branches/opname_classes3/filter/filter/term_grammar.ml
+8 -3 metaprl-branches/opname_classes3/filter/filter/term_grammar.mli
+1 -0 metaprl-branches/opname_classes3/filter/phobos/phobos_constants.ml
+1 -1 metaprl-branches/opname_classes3/filter/phobos/phobos_parser.mly
+29 -26 metaprl-branches/opname_classes3/library/basic.ml
+52 -49 metaprl-branches/opname_classes3/library/db.ml
+17 -15 metaprl-branches/opname_classes3/library/definition.ml
+9 -7 metaprl-branches/opname_classes3/library/library.ml
+5 -3 metaprl-branches/opname_classes3/library/link.ml
+6 -4 metaprl-branches/opname_classes3/library/mbterm.ml
+58 -36 metaprl-branches/opname_classes3/library/nuprl5.ml
+40 -38 metaprl-branches/opname_classes3/library/orb.ml
+32 -12 metaprl-branches/opname_classes3/refiner/refbase/opname.ml
+13 -4 metaprl-branches/opname_classes3/refiner/refbase/opname.mli
+2 -2 metaprl-branches/opname_classes3/refiner/refiner/refine.ml
+2 -2 metaprl-branches/opname_classes3/refiner/refiner/refine.mli
+24 -11 metaprl-branches/opname_classes3/refiner/refiner/refine_error.ml
+4 -4 metaprl-branches/opname_classes3/refiner/refiner/refine_error.mli
+193 -61 metaprl-branches/opname_classes3/refiner/refiner/refiner_debug.ml
+9 -1 metaprl-branches/opname_classes3/refiner/refiner/refiner_ds.ml
+9 -2 metaprl-branches/opname_classes3/refiner/refiner/refiner_std.ml
+1 -0 metaprl-branches/opname_classes3/refiner/reflib/Files
+98 -25 metaprl-branches/opname_classes3/refiner/reflib/ascii_io.ml
+11 -4 metaprl-branches/opname_classes3/refiner/reflib/dform.ml
+1 -0 metaprl-branches/opname_classes3/refiner/reflib/jall.ml
+1 -0 metaprl-branches/opname_classes3/refiner/reflib/lib_term.ml
+200 -126 metaprl-branches/opname_classes3/refiner/reflib/refine_exn.ml
+121 -107 metaprl-branches/opname_classes3/refiner/reflib/simple_print.ml
+10 -10 metaprl-branches/opname_classes3/refiner/reflib/term_compare.ml
+103 -69 metaprl-branches/opname_classes3/refiner/reflib/term_match_table.ml
+5 -1 metaprl-branches/opname_classes3/refiner/reflib/term_match_table.mli
+124 -124 metaprl-branches/opname_classes3/refiner/reflib/term_order.ml
Added metaprl-branches/opname_classes3/refiner/reflib/term_ty_infer.ml
Properties metaprl-branches/opname_classes3/refiner/reflib/term_ty_infer.ml
Added metaprl-branches/opname_classes3/refiner/reflib/term_ty_infer.mli
Properties metaprl-branches/opname_classes3/refiner/reflib/term_ty_infer.mli
+1 -0 metaprl-branches/opname_classes3/refiner/reflib/unify_mm.ml
+1 -0 metaprl-branches/opname_classes3/refiner/refsig/Files
+27 -8 metaprl-branches/opname_classes3/refiner/refsig/refine_error_sig.ml
+8 -2 metaprl-branches/opname_classes3/refiner/refsig/refiner_sig.ml
+4 -2 metaprl-branches/opname_classes3/refiner/refsig/rewrite_sig.ml
Added metaprl-branches/opname_classes3/refiner/refsig/term_eval_sig.ml
Properties metaprl-branches/opname_classes3/refiner/refsig/term_eval_sig.ml
+10 -0 metaprl-branches/opname_classes3/refiner/refsig/term_man_sig.ml
+3 -0 metaprl-branches/opname_classes3/refiner/refsig/term_meta_sig.ml
+8 -4 metaprl-branches/opname_classes3/refiner/refsig/term_op_sig.ml
+3 -0 metaprl-branches/opname_classes3/refiner/refsig/term_shape_sig.ml
+36 -13 metaprl-branches/opname_classes3/refiner/refsig/term_sig.ml
Added metaprl-branches/opname_classes3/refiner/refsig/term_ty_sig.ml
Properties metaprl-branches/opname_classes3/refiner/refsig/term_ty_sig.ml
+26 -14 metaprl-branches/opname_classes3/refiner/rewrite/rewrite.ml
+1 -1 metaprl-branches/opname_classes3/refiner/rewrite/rewrite.mli
+2 -2 metaprl-branches/opname_classes3/refiner/rewrite/rewrite_build_contractum.ml
+1 -1 metaprl-branches/opname_classes3/refiner/rewrite/rewrite_build_contractum.mli
+1 -1 metaprl-branches/opname_classes3/refiner/rewrite/rewrite_compile_contractum.ml
+1 -1 metaprl-branches/opname_classes3/refiner/rewrite/rewrite_compile_contractum.mli
+14 -14 metaprl-branches/opname_classes3/refiner/rewrite/rewrite_compile_redex.ml
+1 -1 metaprl-branches/opname_classes3/refiner/rewrite/rewrite_compile_redex.mli
+5 -3 metaprl-branches/opname_classes3/refiner/rewrite/rewrite_debug.ml
+1 -1 metaprl-branches/opname_classes3/refiner/rewrite/rewrite_debug.mli
+5 -4 metaprl-branches/opname_classes3/refiner/rewrite/rewrite_match_redex.ml
+1 -1 metaprl-branches/opname_classes3/refiner/rewrite/rewrite_match_redex.mli
+6 -4 metaprl-branches/opname_classes3/refiner/rewrite/rewrite_meta.ml
+1 -1 metaprl-branches/opname_classes3/refiner/rewrite/rewrite_meta.mli
+2 -1 metaprl-branches/opname_classes3/refiner/rewrite/rewrite_types.ml
+1 -1 metaprl-branches/opname_classes3/refiner/rewrite/rewrite_util.ml
+1 -1 metaprl-branches/opname_classes3/refiner/rewrite/rewrite_util.mli
+3 -3 metaprl-branches/opname_classes3/refiner/term_ds/term_addr_ds.ml
+2 -2 metaprl-branches/opname_classes3/refiner/term_ds/term_addr_ds.mli
+4 -4 metaprl-branches/opname_classes3/refiner/term_ds/term_base_ds.ml
+4 -4 metaprl-branches/opname_classes3/refiner/term_ds/term_base_ds.mli
+6 -6 metaprl-branches/opname_classes3/refiner/term_ds/term_ds.ml
+6 -6 metaprl-branches/opname_classes3/refiner/term_ds/term_ds_sig.ml
Added metaprl-branches/opname_classes3/refiner/term_ds/term_eval_ds.ml
Properties metaprl-branches/opname_classes3/refiner/term_ds/term_eval_ds.ml
Added metaprl-branches/opname_classes3/refiner/term_ds/term_eval_ds.mli
Properties metaprl-branches/opname_classes3/refiner/term_ds/term_eval_ds.mli
+105 -4 metaprl-branches/opname_classes3/refiner/term_ds/term_man_ds.ml
+2 -2 metaprl-branches/opname_classes3/refiner/term_ds/term_man_ds.mli
+28 -4 metaprl-branches/opname_classes3/refiner/term_ds/term_op_ds.ml
+6 -5 metaprl-branches/opname_classes3/refiner/term_ds/term_op_ds.mli
+8 -6 metaprl-branches/opname_classes3/refiner/term_ds/term_subst_ds.ml
+6 -5 metaprl-branches/opname_classes3/refiner/term_ds/term_subst_ds.mli
+1 -0 metaprl-branches/opname_classes3/refiner/term_gen/Files
+3 -3 metaprl-branches/opname_classes3/refiner/term_gen/term_addr_gen.ml
+2 -2 metaprl-branches/opname_classes3/refiner/term_gen/term_addr_gen.mli
+6 -6 metaprl-branches/opname_classes3/refiner/term_gen/term_hash.ml
+7 -7 metaprl-branches/opname_classes3/refiner/term_gen/term_header_constr.ml
+99 -4 metaprl-branches/opname_classes3/refiner/term_gen/term_man_gen.ml
+1 -1 metaprl-branches/opname_classes3/refiner/term_gen/term_man_gen.mli
+44 -2 metaprl-branches/opname_classes3/refiner/term_gen/term_meta_gen.ml
+1 -1 metaprl-branches/opname_classes3/refiner/term_gen/term_meta_gen.mli
+32 -5 metaprl-branches/opname_classes3/refiner/term_gen/term_shape_gen.ml
+7 -0 metaprl-branches/opname_classes3/refiner/term_gen/term_shape_gen.mli
Added metaprl-branches/opname_classes3/refiner/term_gen/term_ty_gen.ml
Properties metaprl-branches/opname_classes3/refiner/term_gen/term_ty_gen.ml
Added metaprl-branches/opname_classes3/refiner/term_gen/term_ty_gen.mli
Properties metaprl-branches/opname_classes3/refiner/term_gen/term_ty_gen.mli
+1 -1 metaprl-branches/opname_classes3/refiner/term_std/term_base_std.ml
+1 -1 metaprl-branches/opname_classes3/refiner/term_std/term_base_std.mli
Added metaprl-branches/opname_classes3/refiner/term_std/term_eval_std.ml
Properties metaprl-branches/opname_classes3/refiner/term_std/term_eval_std.ml
Added metaprl-branches/opname_classes3/refiner/term_std/term_eval_std.mli
Properties metaprl-branches/opname_classes3/refiner/term_std/term_eval_std.mli
+25 -1 metaprl-branches/opname_classes3/refiner/term_std/term_op_std.ml
+1 -1 metaprl-branches/opname_classes3/refiner/term_std/term_op_std.mli
+6 -6 metaprl-branches/opname_classes3/refiner/term_std/term_std.ml
+6 -6 metaprl-branches/opname_classes3/refiner/term_std/term_std_sig.ml
+5 -5 metaprl-branches/opname_classes3/refiner/term_std/term_subst_std.ml
+1 -1 metaprl-branches/opname_classes3/refiner/term_std/term_subst_std.mli
+172 -11 metaprl-branches/opname_classes3/support/display/perv.ml
+23 -2 metaprl-branches/opname_classes3/support/display/perv.mli
+37 -1 metaprl-branches/opname_classes3/support/display/summary.ml
+4 -1 metaprl-branches/opname_classes3/support/display/summary.mli
+37 -2 metaprl-branches/opname_classes3/support/shell/package_info.ml
+6 -1 metaprl-branches/opname_classes3/support/shell/package_info.mli
+15 -3 metaprl-branches/opname_classes3/support/shell/shell_core.ml
+6 -1 metaprl-branches/opname_classes3/support/shell/shell_package.ml
+75 -15 metaprl-branches/opname_classes3/support/shell/shell_state.ml
+4 -1 metaprl-branches/opname_classes3/support/shell/shell_state.mli
+13 -15 metaprl-branches/opname_classes3/support/tactics/dtactic.ml
+8 -7 metaprl-branches/opname_classes3/support/tactics/top_conversionals.ml
+16 -12 metaprl-branches/opname_classes3/support/tactics/top_tacticals.ml
+0 -0 metaprl-branches/opname_classes3/support/tactics/top_tacticals.mli
+26 -25 metaprl-branches/opname_classes3/theories/base/base_meta.ml
+20 -20 metaprl-branches/opname_classes3/theories/base/base_meta.mli
+3 -3 metaprl-branches/opname_classes3/theories/base/base_reflection.ml
+3 -3 metaprl-branches/opname_classes3/theories/base/base_reflection.mli
+1 -1 metaprl-branches/opname_classes3/theories/base/base_rewrite.ml
+1 -1 metaprl-branches/opname_classes3/theories/base/base_rewrite.mli
+101 -106 metaprl-branches/opname_classes3/theories/cic/cic_ind_cases.ml
+291 -295 metaprl-branches/opname_classes3/theories/cic/cic_ind_type.ml
+85 -85 metaprl-branches/opname_classes3/theories/cic/cic_ind_type.mli
+6 -6 metaprl-branches/opname_classes3/theories/cic/cic_lambda.ml
+4 -4 metaprl-branches/opname_classes3/theories/cic/cic_lambda.mli
+18 -18 metaprl-branches/opname_classes3/theories/cic/cic_list.ml
+1 -0 metaprl-branches/opname_classes3/theories/czf/czf_itt_rel.ml
+3 -3 metaprl-branches/opname_classes3/theories/experimental/compile/m_ast.ml
+1 -1 metaprl-branches/opname_classes3/theories/experimental/compile/m_ast.mli
+4 -4 metaprl-branches/opname_classes3/theories/experimental/compile/m_cps.ml
+1 -1 metaprl-branches/opname_classes3/theories/experimental/compile/m_doc_ir.ml
+1 -1 metaprl-branches/opname_classes3/theories/experimental/compile/m_doc_ir.mli
+2 -2 metaprl-branches/opname_classes3/theories/experimental/compile/m_doc_proposal.ml
+1 -1 metaprl-branches/opname_classes3/theories/experimental/compile/m_doc_proposal.mli
+4 -4 metaprl-branches/opname_classes3/theories/experimental/compile/m_ir.ml
+2 -2 metaprl-branches/opname_classes3/theories/experimental/compile/m_ir.mli
+5 -5 metaprl-branches/opname_classes3/theories/experimental/compile/m_ir_ast.ml
+1 -0 metaprl-branches/opname_classes3/theories/experimental/compile/m_standardize.ml
+10 -8 metaprl-branches/opname_classes3/theories/experimental/compile/m_test.ml
+12 -12 metaprl-branches/opname_classes3/theories/experimental/compile/m_x86_asm.ml
+4 -4 metaprl-branches/opname_classes3/theories/experimental/compile/m_x86_asm.mli
+12 -12 metaprl-branches/opname_classes3/theories/experimental/compile/m_x86_codegen.ml
+11 -11 metaprl-branches/opname_classes3/theories/experimental/compile/m_x86_term.ml
Properties metaprl-branches/opname_classes3/theories/experimental/syntax
Added metaprl-branches/opname_classes3/theories/experimental/syntax/OMakefile
Properties metaprl-branches/opname_classes3/theories/experimental/syntax/OMakefile
Added metaprl-branches/opname_classes3/theories/experimental/syntax/syntax_test.ml
Properties metaprl-branches/opname_classes3/theories/experimental/syntax/syntax_test.ml
Added metaprl-branches/opname_classes3/theories/experimental/syntax/syntax_test.mli
Properties metaprl-branches/opname_classes3/theories/experimental/syntax/syntax_test.mli
+1 -1 metaprl-branches/opname_classes3/theories/fir/mfir_sequent.ml
+1 -1 metaprl-branches/opname_classes3/theories/fir/mfir_sequent.mli
+3 -0 metaprl-branches/opname_classes3/theories/itt/OMakefile
+2 -2 metaprl-branches/opname_classes3/theories/itt/itt_algebra_df.ml
+1 -5 metaprl-branches/opname_classes3/theories/itt/itt_atom.ml
+2 -2 metaprl-branches/opname_classes3/theories/itt/itt_atom.mli
+53 -0 metaprl-branches/opname_classes3/theories/itt/itt_atom.prla
+1 -0 metaprl-branches/opname_classes3/theories/itt/itt_bintree.ml
+53 -0 metaprl-branches/opname_classes3/theories/itt/itt_bintree.prla
+1 -0 metaprl-branches/opname_classes3/theories/itt/itt_closure.ml
+53 -0 metaprl-branches/opname_classes3/theories/itt/itt_closure.prla
+1 -0 metaprl-branches/opname_classes3/theories/itt/itt_cyclic_group.ml
+51 -0 metaprl-branches/opname_classes3/theories/itt/itt_cyclic_group.prla
+1 -0 metaprl-branches/opname_classes3/theories/itt/itt_datatree.ml
+1 -0 metaprl-branches/opname_classes3/theories/itt/itt_derive.ml
+1 -0 metaprl-branches/opname_classes3/theories/itt/itt_field2.ml
+53 -0 metaprl-branches/opname_classes3/theories/itt/itt_field2.prla
+1 -0 metaprl-branches/opname_classes3/theories/itt/itt_field_e.ml
+53 -0 metaprl-branches/opname_classes3/theories/itt/itt_field_e.prla
+2 -2 metaprl-branches/opname_classes3/theories/itt/itt_fun.ml
+1 -0 metaprl-branches/opname_classes3/theories/itt/itt_fun.mli
+1 -0 metaprl-branches/opname_classes3/theories/itt/itt_group.ml
+52 -0 metaprl-branches/opname_classes3/theories/itt/itt_group.prla
+6 -3 metaprl-branches/opname_classes3/theories/itt/itt_grouplikeobj.ml
+53 -0 metaprl-branches/opname_classes3/theories/itt/itt_grouplikeobj.prla
+1 -0 metaprl-branches/opname_classes3/theories/itt/itt_intdomain.ml
+53 -0 metaprl-branches/opname_classes3/theories/itt/itt_intdomain.prla
+1 -0 metaprl-branches/opname_classes3/theories/itt/itt_intdomain_e.ml
+53 -0 metaprl-branches/opname_classes3/theories/itt/itt_intdomain_e.prla
Added metaprl-branches/opname_classes3/theories/itt/itt_labels.mlz
Properties metaprl-branches/opname_classes3/theories/itt/itt_labels.mlz
+54 -0 metaprl-branches/opname_classes3/theories/itt/itt_mpoly.prla
+54 -0 metaprl-branches/opname_classes3/theories/itt/itt_mpoly2.prla
+54 -0 metaprl-branches/opname_classes3/theories/itt/itt_mpoly2_bench.prla
+54 -0 metaprl-branches/opname_classes3/theories/itt/itt_mpoly3.prla
+54 -0 metaprl-branches/opname_classes3/theories/itt/itt_mpoly3_bench.prla
+2 -1 metaprl-branches/opname_classes3/theories/itt/itt_obj_base_rewrite.ml
+53 -0 metaprl-branches/opname_classes3/theories/itt/itt_obj_base_rewrite.prla
+1 -0 metaprl-branches/opname_classes3/theories/itt/itt_order.ml
+51 -0 metaprl-branches/opname_classes3/theories/itt/itt_order.prla
+7 -2 metaprl-branches/opname_classes3/theories/itt/itt_pairwise.ml
+1 -0 metaprl-branches/opname_classes3/theories/itt/itt_poly.ml
+50 -0 metaprl-branches/opname_classes3/theories/itt/itt_poly.prla
+1 -1 metaprl-branches/opname_classes3/theories/itt/itt_prec.mli
+1 -0 metaprl-branches/opname_classes3/theories/itt/itt_quotient_group.ml
+52 -0 metaprl-branches/opname_classes3/theories/itt/itt_quotient_group.prla
+1 -0 metaprl-branches/opname_classes3/theories/itt/itt_rat.ml
+1 -0 metaprl-branches/opname_classes3/theories/itt/itt_rat.mli
+51 -0 metaprl-branches/opname_classes3/theories/itt/itt_rat.prla
+2 -1 metaprl-branches/opname_classes3/theories/itt/itt_rbtree.ml
+1 -0 metaprl-branches/opname_classes3/theories/itt/itt_record.ml
+2 -2 metaprl-branches/opname_classes3/theories/itt/itt_record.mli
+53 -0 metaprl-branches/opname_classes3/theories/itt/itt_record.prla
+1 -0 metaprl-branches/opname_classes3/theories/itt/itt_record_exm.ml
+73 -20 metaprl-branches/opname_classes3/theories/itt/itt_record_exm.prla
+59 -5 metaprl-branches/opname_classes3/theories/itt/itt_record_label.prla
+11 -10 metaprl-branches/opname_classes3/theories/itt/itt_record_renaming.ml
+55 -3 metaprl-branches/opname_classes3/theories/itt/itt_record_renaming.prla
+1 -0 metaprl-branches/opname_classes3/theories/itt/itt_relation_str.ml
+6 -3 metaprl-branches/opname_classes3/theories/itt/itt_ring2.ml
+53 -0 metaprl-branches/opname_classes3/theories/itt/itt_ring2.prla
+1 -0 metaprl-branches/opname_classes3/theories/itt/itt_ring_e.ml
+53 -0 metaprl-branches/opname_classes3/theories/itt/itt_ring_e.prla
+1 -0 metaprl-branches/opname_classes3/theories/itt/itt_ring_uce.ml
+52 -0 metaprl-branches/opname_classes3/theories/itt/itt_ring_uce.prla
+3 -2 metaprl-branches/opname_classes3/theories/itt/itt_set_str.ml
+1 -0 metaprl-branches/opname_classes3/theories/itt/itt_sortedtree.ml
+66 -14 metaprl-branches/opname_classes3/theories/itt/itt_sortedtree.prla
+10 -3 metaprl-branches/opname_classes3/theories/itt/itt_test.ml
+1 -0 metaprl-branches/opname_classes3/theories/itt/itt_unitring.ml
+53 -0 metaprl-branches/opname_classes3/theories/itt/itt_unitring.prla
+2 -15 metaprl-branches/opname_classes3/theories/phobos/phobos_theory.ml
+0 -0 metaprl-branches/opname_classes3/theories/sil/sil_program.ml
+5 -0 metaprl-branches/opname_classes3/theories/sil/sil_programs.ml
+5 -0 metaprl-branches/opname_classes3/theories/sil/sil_programs.mli
+0 -0 metaprl-branches/opname_classes3/theories/sil/sil_sos.ml
+0 -0 metaprl-branches/opname_classes3/theories/sil/sil_state.ml
+1 -0 metaprl-branches/opname_classes3/theories/tptp/tptp.ml
+7001 -8113 metaprl-branches/opname_classes3/theories/tptp/tptp.prla
+1 -0 metaprl-branches/opname_classes3/theories/tptp/tptp_cache.ml
+4 -2 metaprl-branches/opname_classes3/util/gen_refiner_debug.pl
+4 -1 metaprl-branches/opname_classes3/util/gen_refiner_debug_err.pl
+121 -160 mpcompiler-branches/opname_classes3/mmc/arch/x86/mmc_x86_asm.ml
+73 -41 mpcompiler-branches/opname_classes3/mmc/arch/x86/mmc_x86_asm.mli
+1 -1 mpcompiler-branches/opname_classes3/mmc/arch/x86/mmc_x86_hoist.ml
+22 -20 mpcompiler-branches/opname_classes3/mmc/arch/x86/mmc_x86_slop.ml
+3 -3 mpcompiler-branches/opname_classes3/mmc/base/mmc_base_dform.ml
+1 -1 mpcompiler-branches/opname_classes3/mmc/base/mmc_base_hoist.ml
+1 -1 mpcompiler-branches/opname_classes3/mmc/base/mmc_base_hoist.mli
+0 -23 mpcompiler-branches/opname_classes3/mmc/base/mmc_base_judgment.ml
+34 -4 mpcompiler-branches/opname_classes3/mmc/base/mmc_base_judgment.mli
+1 -1 mpcompiler-branches/opname_classes3/mmc/base/mmc_base_meta.ml
+1 -1 mpcompiler-branches/opname_classes3/mmc/base/mmc_base_meta.mli
+1 -1 mpcompiler-branches/opname_classes3/mmc/base/mmc_base_standardize.ml
+0 -2 mpcompiler-branches/opname_classes3/mmc/core/Files
+12 -70 mpcompiler-branches/opname_classes3/mmc/core/mmc_core_ast.ml
+56 -38 mpcompiler-branches/opname_classes3/mmc/core/mmc_core_ast.mli
+1 -2 mpcompiler-branches/opname_classes3/mmc/core/mmc_core_closure.ml
+1 -1 mpcompiler-branches/opname_classes3/mmc/core/mmc_core_closure.mli
+0 -2 mpcompiler-branches/opname_classes3/mmc/core/mmc_core_cps.ml
+4 -4 mpcompiler-branches/opname_classes3/mmc/core/mmc_core_cps.mli
+1 -1 mpcompiler-branches/opname_classes3/mmc/core/mmc_core_front.mli
+7 -7 mpcompiler-branches/opname_classes3/mmc/core/mmc_core_grammar.ml
+7 -7 mpcompiler-branches/opname_classes3/mmc/core/mmc_core_grammar.mli
+5 -3 mpcompiler-branches/opname_classes3/mmc/core/mmc_core_inline.mli
+2 -1 mpcompiler-branches/opname_classes3/mmc/core/mmc_core_list_util.ml
+2 -1 mpcompiler-branches/opname_classes3/mmc/core/mmc_core_list_util.mli
+2 -2 mpcompiler-branches/opname_classes3/mmc/core/mmc_core_reserve.mli
+216 -32 mpcompiler-branches/opname_classes3/mmc/core/mmc_core_sweep_ty.ml
+16 -46 mpcompiler-branches/opname_classes3/mmc/core/mmc_core_tast.ml
+47 -13 mpcompiler-branches/opname_classes3/mmc/core/mmc_core_tast.mli
+1 -1 mpcompiler-branches/opname_classes3/mmc/core/mmc_core_tast_util.ml
+100 -78 mpcompiler-branches/opname_classes3/mmc/core/mmc_core_type_check.ml
+14 -8 mpcompiler-branches/opname_classes3/mmc/core/mmc_core_type_check.mli
+36 -28 mpcompiler-branches/opname_classes3/mmc/core/mmc_core_type_erase.ml
+5 -1 mpcompiler-branches/opname_classes3/mmc/core/mmc_core_type_erase.mli
+17 -19 mpcompiler-branches/opname_classes3/mmc/core/mmc_core_type_infer.ml
+9 -14 mpcompiler-branches/opname_classes3/mmc/core/mmc_core_value.ml
+6 -4 mpcompiler-branches/opname_classes3/mmc/core/mmc_core_value.mli
+21 -15 mpcompiler-branches/opname_classes3/mmc/extensions/bool/mmc_ext_bool.mli
+34 -31 mpcompiler-branches/opname_classes3/mmc/extensions/int/mmc_ext_int.mli
+39 -7 mpcompiler-branches/opname_classes3/mmc/extensions/operator/mmc_ext_operator.mli
+2 -2 mpcompiler-branches/opname_classes3/mmc/extensions/special/mmc_ext_special.ml
+2 -2 mpcompiler-branches/opname_classes3/mmc/extensions/special/mmc_ext_special.mli
+1 -6 mpcompiler-branches/opname_classes3/mmc/extensions/string/mmc_ext_string.ml
+5 -2 mpcompiler-branches/opname_classes3/mmc/extensions/string/mmc_ext_string.mli
+5 -4 mpcompiler-branches/opname_classes3/mmc/extensions/tyexists/mmc_ext_tyexists.ml
+4 -3 mpcompiler-branches/opname_classes3/mmc/extensions/tyexists/mmc_ext_tyexists.mli
+0 -1 mpcompiler-branches/opname_classes3/util/Files
+9 -8 mpcompiler-branches/opname_classes3/util/mm_arith_util.ml
+8 -7 mpcompiler-branches/opname_classes3/util/mm_arith_util.mli
+6 -5 mpcompiler-branches/opname_classes3/util/mm_dform_util.ml
+4 -4 mpcompiler-branches/opname_classes3/util/mm_dform_util.mli
+16 -9 mpcompiler-branches/opname_classes3/util/mm_list_util.ml
+10 -6 mpcompiler-branches/opname_classes3/util/mm_list_util.mli
Deleted mpcompiler-branches/opname_classes3/util/mmc_term_util.ml
Deleted mpcompiler-branches/opname_classes3/util/mmc_term_util.mli