Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-03 18:14:03 -0800 (Thu, 03 Feb 2005)
Revision: 6587
Log message:

      Yet another instance of the opname_classes branch, merged once again with the
      trunk changes and re-branched.
      
      Known issues:
       - The .mli opname declarations are added to the .cmoz in the reverse order.
         This, among other things causes Failure ("unknown typeclass:
         Mmc_base_judgment!Prop") exception on cd'ing into the /mmc_base_judgment
         module.
       - The .mli opname declarations are added to the .cmoz even when .cmoz has its
         own copy. That results in the "ls" output (and other things, such as .cmoz
         and .prla files) being unnecessarily cluttered.
       - If the same shape is declared several times (possibly with incompatible
         types), does anybody notice?
      
      Potential TODOs and RFEs:
       - Proper type checking for display forms.
       - Could we may be come up with a way to propagate certain declarations from
         .ml into .cmiz (instead of the other way around)? Some declarations needs
         to stay in the .ml in order to get properly documented.
       - "declare sequent" shortcuts:
          - when the type is { Term : Term >- Term } : Term, allow omitting it
          - when the type is { Term : Term >- Term } : Foo, allow typing just ": Foo"
       - Perv!nil/Perv!cons should have the Dform type.
          - When the sequent conclusion is omitted, a we should use something other
            than Perv!nil for the conclusion. This new "default conclusion" term
            should be a member of a singleton type (in the Term typeclass), and MMC
            should be using that in the type of Mmc_core_ast!ty_args
          - Base_reflection should use its own cons and nil for bterm lists.
       - The new stuff (both the new syntax and the typechecking algorithm) need to
         be documented.
      

Changes  Path
+54 -52 metaprl-branches/opname_classes4/editor/ml/nuprl_eval.ml
+3 -1 metaprl-branches/opname_classes4/editor/ml/nuprl_jprover.ml
+703 -155 metaprl-branches/opname_classes4/filter/base/filter_cache_fun.ml
+1 -0 metaprl-branches/opname_classes4/filter/base/filter_cache_fun.mli
+55 -19 metaprl-branches/opname_classes4/filter/base/filter_exn.ml
+3 -2 metaprl-branches/opname_classes4/filter/base/filter_exn.mli
+41 -0 metaprl-branches/opname_classes4/filter/base/filter_grammar.ml
+7 -0 metaprl-branches/opname_classes4/filter/base/filter_grammar.mli
+6 -4 metaprl-branches/opname_classes4/filter/base/filter_magic.ml
+464 -49 metaprl-branches/opname_classes4/filter/base/filter_summary.ml
+13 -3 metaprl-branches/opname_classes4/filter/base/filter_summary_type.ml
+98 -22 metaprl-branches/opname_classes4/filter/base/filter_type.ml
+7 -11 metaprl-branches/opname_classes4/filter/base/filter_util.ml
+0 -2 metaprl-branches/opname_classes4/filter/base/filter_util.mli
+769 -421 metaprl-branches/opname_classes4/filter/filter/filter_parse.ml
+23 -15 metaprl-branches/opname_classes4/filter/filter/filter_patt.ml
+39 -9 metaprl-branches/opname_classes4/filter/filter/filter_prog.ml
+559 -150 metaprl-branches/opname_classes4/filter/filter/term_grammar.ml
+5 -3 metaprl-branches/opname_classes4/filter/filter/term_grammar.mli
+1 -0 metaprl-branches/opname_classes4/filter/phobos/phobos_constants.ml
+1 -1 metaprl-branches/opname_classes4/filter/phobos/phobos_parser.mly
+29 -26 metaprl-branches/opname_classes4/library/basic.ml
+52 -49 metaprl-branches/opname_classes4/library/db.ml
+17 -15 metaprl-branches/opname_classes4/library/definition.ml
+9 -7 metaprl-branches/opname_classes4/library/library.ml
+5 -3 metaprl-branches/opname_classes4/library/link.ml
+6 -4 metaprl-branches/opname_classes4/library/mbterm.ml
+58 -36 metaprl-branches/opname_classes4/library/nuprl5.ml
+40 -38 metaprl-branches/opname_classes4/library/orb.ml
+32 -12 metaprl-branches/opname_classes4/refiner/refbase/opname.ml
+13 -4 metaprl-branches/opname_classes4/refiner/refbase/opname.mli
+2 -2 metaprl-branches/opname_classes4/refiner/refiner/refine.ml
+2 -2 metaprl-branches/opname_classes4/refiner/refiner/refine.mli
+24 -11 metaprl-branches/opname_classes4/refiner/refiner/refine_error.ml
+4 -4 metaprl-branches/opname_classes4/refiner/refiner/refine_error.mli
+200 -64 metaprl-branches/opname_classes4/refiner/refiner/refiner_debug.ml
+9 -1 metaprl-branches/opname_classes4/refiner/refiner/refiner_ds.ml
+9 -2 metaprl-branches/opname_classes4/refiner/refiner/refiner_std.ml
+1 -0 metaprl-branches/opname_classes4/refiner/reflib/Files
+33 -24 metaprl-branches/opname_classes4/refiner/reflib/ascii_io.ml
+12 -4 metaprl-branches/opname_classes4/refiner/reflib/dform.ml
+1 -0 metaprl-branches/opname_classes4/refiner/reflib/jall.ml
+1 -0 metaprl-branches/opname_classes4/refiner/reflib/lib_term.ml
+200 -126 metaprl-branches/opname_classes4/refiner/reflib/refine_exn.ml
+121 -107 metaprl-branches/opname_classes4/refiner/reflib/simple_print.ml
+10 -10 metaprl-branches/opname_classes4/refiner/reflib/term_compare.ml
+103 -69 metaprl-branches/opname_classes4/refiner/reflib/term_match_table.ml
+5 -1 metaprl-branches/opname_classes4/refiner/reflib/term_match_table.mli
+124 -124 metaprl-branches/opname_classes4/refiner/reflib/term_order.ml
Added metaprl-branches/opname_classes4/refiner/reflib/term_ty_infer.ml
Properties metaprl-branches/opname_classes4/refiner/reflib/term_ty_infer.ml
Added metaprl-branches/opname_classes4/refiner/reflib/term_ty_infer.mli
Properties metaprl-branches/opname_classes4/refiner/reflib/term_ty_infer.mli
+1 -0 metaprl-branches/opname_classes4/refiner/reflib/unify_mm.ml
+1 -0 metaprl-branches/opname_classes4/refiner/refsig/Files
+27 -8 metaprl-branches/opname_classes4/refiner/refsig/refine_error_sig.ml
+8 -2 metaprl-branches/opname_classes4/refiner/refsig/refiner_sig.ml
+4 -2 metaprl-branches/opname_classes4/refiner/refsig/rewrite_sig.ml
Added metaprl-branches/opname_classes4/refiner/refsig/term_eval_sig.ml
Properties metaprl-branches/opname_classes4/refiner/refsig/term_eval_sig.ml
+10 -0 metaprl-branches/opname_classes4/refiner/refsig/term_man_sig.ml
+5 -0 metaprl-branches/opname_classes4/refiner/refsig/term_meta_sig.ml
+8 -4 metaprl-branches/opname_classes4/refiner/refsig/term_op_sig.ml
+3 -0 metaprl-branches/opname_classes4/refiner/refsig/term_shape_sig.ml
+37 -14 metaprl-branches/opname_classes4/refiner/refsig/term_sig.ml
Added metaprl-branches/opname_classes4/refiner/refsig/term_ty_sig.ml
Properties metaprl-branches/opname_classes4/refiner/refsig/term_ty_sig.ml
+26 -14 metaprl-branches/opname_classes4/refiner/rewrite/rewrite.ml
+1 -1 metaprl-branches/opname_classes4/refiner/rewrite/rewrite.mli
+2 -2 metaprl-branches/opname_classes4/refiner/rewrite/rewrite_build_contractum.ml
+1 -1 metaprl-branches/opname_classes4/refiner/rewrite/rewrite_build_contractum.mli
+1 -1 metaprl-branches/opname_classes4/refiner/rewrite/rewrite_compile_contractum.ml
+1 -1 metaprl-branches/opname_classes4/refiner/rewrite/rewrite_compile_contractum.mli
+14 -14 metaprl-branches/opname_classes4/refiner/rewrite/rewrite_compile_redex.ml
+1 -1 metaprl-branches/opname_classes4/refiner/rewrite/rewrite_compile_redex.mli
+5 -3 metaprl-branches/opname_classes4/refiner/rewrite/rewrite_debug.ml
+1 -1 metaprl-branches/opname_classes4/refiner/rewrite/rewrite_debug.mli
+5 -4 metaprl-branches/opname_classes4/refiner/rewrite/rewrite_match_redex.ml
+1 -1 metaprl-branches/opname_classes4/refiner/rewrite/rewrite_match_redex.mli
+6 -4 metaprl-branches/opname_classes4/refiner/rewrite/rewrite_meta.ml
+1 -1 metaprl-branches/opname_classes4/refiner/rewrite/rewrite_meta.mli
+2 -1 metaprl-branches/opname_classes4/refiner/rewrite/rewrite_types.ml
+1 -1 metaprl-branches/opname_classes4/refiner/rewrite/rewrite_util.ml
+1 -1 metaprl-branches/opname_classes4/refiner/rewrite/rewrite_util.mli
+3 -3 metaprl-branches/opname_classes4/refiner/term_ds/term_addr_ds.ml
+2 -2 metaprl-branches/opname_classes4/refiner/term_ds/term_addr_ds.mli
+4 -4 metaprl-branches/opname_classes4/refiner/term_ds/term_base_ds.ml
+4 -4 metaprl-branches/opname_classes4/refiner/term_ds/term_base_ds.mli
+7 -7 metaprl-branches/opname_classes4/refiner/term_ds/term_ds.ml
+7 -7 metaprl-branches/opname_classes4/refiner/term_ds/term_ds_sig.ml
Added metaprl-branches/opname_classes4/refiner/term_ds/term_eval_ds.ml
Properties metaprl-branches/opname_classes4/refiner/term_ds/term_eval_ds.ml
Added metaprl-branches/opname_classes4/refiner/term_ds/term_eval_ds.mli
Properties metaprl-branches/opname_classes4/refiner/term_ds/term_eval_ds.mli
+114 -10 metaprl-branches/opname_classes4/refiner/term_ds/term_man_ds.ml
+2 -2 metaprl-branches/opname_classes4/refiner/term_ds/term_man_ds.mli
+28 -4 metaprl-branches/opname_classes4/refiner/term_ds/term_op_ds.ml
+6 -5 metaprl-branches/opname_classes4/refiner/term_ds/term_op_ds.mli
+8 -6 metaprl-branches/opname_classes4/refiner/term_ds/term_subst_ds.ml
+6 -5 metaprl-branches/opname_classes4/refiner/term_ds/term_subst_ds.mli
+1 -0 metaprl-branches/opname_classes4/refiner/term_gen/Files
+3 -3 metaprl-branches/opname_classes4/refiner/term_gen/term_addr_gen.ml
+2 -2 metaprl-branches/opname_classes4/refiner/term_gen/term_addr_gen.mli
+6 -6 metaprl-branches/opname_classes4/refiner/term_gen/term_hash.ml
+7 -7 metaprl-branches/opname_classes4/refiner/term_gen/term_header_constr.ml
+100 -5 metaprl-branches/opname_classes4/refiner/term_gen/term_man_gen.ml
+1 -1 metaprl-branches/opname_classes4/refiner/term_gen/term_man_gen.mli
+61 -3 metaprl-branches/opname_classes4/refiner/term_gen/term_meta_gen.ml
+1 -1 metaprl-branches/opname_classes4/refiner/term_gen/term_meta_gen.mli
+32 -5 metaprl-branches/opname_classes4/refiner/term_gen/term_shape_gen.ml
+7 -0 metaprl-branches/opname_classes4/refiner/term_gen/term_shape_gen.mli
Added metaprl-branches/opname_classes4/refiner/term_gen/term_ty_gen.ml
Properties metaprl-branches/opname_classes4/refiner/term_gen/term_ty_gen.ml
Added metaprl-branches/opname_classes4/refiner/term_gen/term_ty_gen.mli
Properties metaprl-branches/opname_classes4/refiner/term_gen/term_ty_gen.mli
+1 -1 metaprl-branches/opname_classes4/refiner/term_std/term_base_std.ml
+1 -1 metaprl-branches/opname_classes4/refiner/term_std/term_base_std.mli
Added metaprl-branches/opname_classes4/refiner/term_std/term_eval_std.ml
Properties metaprl-branches/opname_classes4/refiner/term_std/term_eval_std.ml
Added metaprl-branches/opname_classes4/refiner/term_std/term_eval_std.mli
Properties metaprl-branches/opname_classes4/refiner/term_std/term_eval_std.mli
+25 -1 metaprl-branches/opname_classes4/refiner/term_std/term_op_std.ml
+1 -1 metaprl-branches/opname_classes4/refiner/term_std/term_op_std.mli
+7 -7 metaprl-branches/opname_classes4/refiner/term_std/term_std.ml
+7 -7 metaprl-branches/opname_classes4/refiner/term_std/term_std_sig.ml
+5 -5 metaprl-branches/opname_classes4/refiner/term_std/term_subst_std.ml
+1 -1 metaprl-branches/opname_classes4/refiner/term_std/term_subst_std.mli
+217 -201 metaprl-branches/opname_classes4/support/display/comment.ml
+189 -187 metaprl-branches/opname_classes4/support/display/comment.mli
+114 -106 metaprl-branches/opname_classes4/support/display/perv.ml
+164 -44 metaprl-branches/opname_classes4/support/display/perv.mli
+117 -91 metaprl-branches/opname_classes4/support/display/summary.ml
+10 -64 metaprl-branches/opname_classes4/support/display/summary.mli
+37 -2 metaprl-branches/opname_classes4/support/shell/package_info.ml
+6 -1 metaprl-branches/opname_classes4/support/shell/package_info.mli
+0 -12 metaprl-branches/opname_classes4/support/shell/proof_edit.ml
+15 -3 metaprl-branches/opname_classes4/support/shell/shell_core.ml
+7 -12 metaprl-branches/opname_classes4/support/shell/shell_package.ml
+75 -15 metaprl-branches/opname_classes4/support/shell/shell_state.ml
+4 -1 metaprl-branches/opname_classes4/support/shell/shell_state.mli
+13 -15 metaprl-branches/opname_classes4/support/tactics/dtactic.ml
+8 -7 metaprl-branches/opname_classes4/support/tactics/top_conversionals.ml
+16 -12 metaprl-branches/opname_classes4/support/tactics/top_tacticals.ml
+0 -0 metaprl-branches/opname_classes4/support/tactics/top_tacticals.mli
+26 -25 metaprl-branches/opname_classes4/theories/base/base_meta.ml
+20 -20 metaprl-branches/opname_classes4/theories/base/base_meta.mli
+3 -3 metaprl-branches/opname_classes4/theories/base/base_reflection.ml
+2 -2 metaprl-branches/opname_classes4/theories/base/base_reflection.mli
+1 -1 metaprl-branches/opname_classes4/theories/base/base_rewrite.ml
+1 -1 metaprl-branches/opname_classes4/theories/base/base_rewrite.mli
+101 -106 metaprl-branches/opname_classes4/theories/cic/cic_ind_cases.ml
+291 -295 metaprl-branches/opname_classes4/theories/cic/cic_ind_type.ml
+85 -85 metaprl-branches/opname_classes4/theories/cic/cic_ind_type.mli
+6 -6 metaprl-branches/opname_classes4/theories/cic/cic_lambda.ml
+4 -4 metaprl-branches/opname_classes4/theories/cic/cic_lambda.mli
+18 -18 metaprl-branches/opname_classes4/theories/cic/cic_list.ml
+1 -0 metaprl-branches/opname_classes4/theories/czf/czf_itt_rel.ml
+3 -3 metaprl-branches/opname_classes4/theories/experimental/compile/m_ast.ml
+1 -1 metaprl-branches/opname_classes4/theories/experimental/compile/m_ast.mli
+4 -4 metaprl-branches/opname_classes4/theories/experimental/compile/m_cps.ml
+1 -1 metaprl-branches/opname_classes4/theories/experimental/compile/m_doc_ir.ml
+1 -1 metaprl-branches/opname_classes4/theories/experimental/compile/m_doc_ir.mli
+2 -2 metaprl-branches/opname_classes4/theories/experimental/compile/m_doc_proposal.ml
+1 -1 metaprl-branches/opname_classes4/theories/experimental/compile/m_doc_proposal.mli
+4 -4 metaprl-branches/opname_classes4/theories/experimental/compile/m_ir.ml
+2 -2 metaprl-branches/opname_classes4/theories/experimental/compile/m_ir.mli
+5 -5 metaprl-branches/opname_classes4/theories/experimental/compile/m_ir_ast.ml
+1 -0 metaprl-branches/opname_classes4/theories/experimental/compile/m_standardize.ml
+10 -8 metaprl-branches/opname_classes4/theories/experimental/compile/m_test.ml
+12 -12 metaprl-branches/opname_classes4/theories/experimental/compile/m_x86_asm.ml
+4 -4 metaprl-branches/opname_classes4/theories/experimental/compile/m_x86_asm.mli
+12 -12 metaprl-branches/opname_classes4/theories/experimental/compile/m_x86_codegen.ml
+11 -11 metaprl-branches/opname_classes4/theories/experimental/compile/m_x86_term.ml
Properties metaprl-branches/opname_classes4/theories/experimental/syntax
Added metaprl-branches/opname_classes4/theories/experimental/syntax/OMakefile
Properties metaprl-branches/opname_classes4/theories/experimental/syntax/OMakefile
Added metaprl-branches/opname_classes4/theories/experimental/syntax/syntax_test.ml
Properties metaprl-branches/opname_classes4/theories/experimental/syntax/syntax_test.ml
Added metaprl-branches/opname_classes4/theories/experimental/syntax/syntax_test.mli
Properties metaprl-branches/opname_classes4/theories/experimental/syntax/syntax_test.mli
+1 -1 metaprl-branches/opname_classes4/theories/fir/mfir_sequent.ml
+1 -1 metaprl-branches/opname_classes4/theories/fir/mfir_sequent.mli
+3 -0 metaprl-branches/opname_classes4/theories/itt/OMakefile
+2 -2 metaprl-branches/opname_classes4/theories/itt/itt_algebra_df.ml
+1 -5 metaprl-branches/opname_classes4/theories/itt/itt_atom.ml
+2 -2 metaprl-branches/opname_classes4/theories/itt/itt_atom.mli
+53 -0 metaprl-branches/opname_classes4/theories/itt/itt_atom.prla
+1 -0 metaprl-branches/opname_classes4/theories/itt/itt_bintree.ml
+52 -0 metaprl-branches/opname_classes4/theories/itt/itt_bintree.prla
+1 -0 metaprl-branches/opname_classes4/theories/itt/itt_closure.ml
+52 -0 metaprl-branches/opname_classes4/theories/itt/itt_closure.prla
+1 -0 metaprl-branches/opname_classes4/theories/itt/itt_cyclic_group.ml
+50 -0 metaprl-branches/opname_classes4/theories/itt/itt_cyclic_group.prla
+1 -0 metaprl-branches/opname_classes4/theories/itt/itt_datatree.ml
+1 -0 metaprl-branches/opname_classes4/theories/itt/itt_derive.ml
+1 -0 metaprl-branches/opname_classes4/theories/itt/itt_field2.ml
+52 -0 metaprl-branches/opname_classes4/theories/itt/itt_field2.prla
+1 -0 metaprl-branches/opname_classes4/theories/itt/itt_field_e.ml
+52 -0 metaprl-branches/opname_classes4/theories/itt/itt_field_e.prla
+2 -2 metaprl-branches/opname_classes4/theories/itt/itt_fun.ml
+1 -0 metaprl-branches/opname_classes4/theories/itt/itt_group.ml
+51 -0 metaprl-branches/opname_classes4/theories/itt/itt_group.prla
+6 -3 metaprl-branches/opname_classes4/theories/itt/itt_grouplikeobj.ml
+52 -0 metaprl-branches/opname_classes4/theories/itt/itt_grouplikeobj.prla
+1 -0 metaprl-branches/opname_classes4/theories/itt/itt_intdomain.ml
+52 -0 metaprl-branches/opname_classes4/theories/itt/itt_intdomain.prla
+1 -0 metaprl-branches/opname_classes4/theories/itt/itt_intdomain_e.ml
+52 -0 metaprl-branches/opname_classes4/theories/itt/itt_intdomain_e.prla
Added metaprl-branches/opname_classes4/theories/itt/itt_labels.mlz
Properties metaprl-branches/opname_classes4/theories/itt/itt_labels.mlz
+53 -0 metaprl-branches/opname_classes4/theories/itt/itt_mpoly.prla
+53 -0 metaprl-branches/opname_classes4/theories/itt/itt_mpoly2.prla
+53 -0 metaprl-branches/opname_classes4/theories/itt/itt_mpoly2_bench.prla
+53 -0 metaprl-branches/opname_classes4/theories/itt/itt_mpoly3.prla
+53 -0 metaprl-branches/opname_classes4/theories/itt/itt_mpoly3_bench.prla
+2 -1 metaprl-branches/opname_classes4/theories/itt/itt_obj_base_rewrite.ml
+52 -0 metaprl-branches/opname_classes4/theories/itt/itt_obj_base_rewrite.prla
+1 -0 metaprl-branches/opname_classes4/theories/itt/itt_order.ml
+50 -0 metaprl-branches/opname_classes4/theories/itt/itt_order.prla
+7 -2 metaprl-branches/opname_classes4/theories/itt/itt_pairwise.ml
+1 -0 metaprl-branches/opname_classes4/theories/itt/itt_poly.ml
+49 -0 metaprl-branches/opname_classes4/theories/itt/itt_poly.prla
+1 -1 metaprl-branches/opname_classes4/theories/itt/itt_prec.mli
+1 -0 metaprl-branches/opname_classes4/theories/itt/itt_quotient_group.ml
+51 -0 metaprl-branches/opname_classes4/theories/itt/itt_quotient_group.prla
+1 -0 metaprl-branches/opname_classes4/theories/itt/itt_rat.ml
+1 -0 metaprl-branches/opname_classes4/theories/itt/itt_rat.mli
+50 -0 metaprl-branches/opname_classes4/theories/itt/itt_rat.prla
+2 -1 metaprl-branches/opname_classes4/theories/itt/itt_rbtree.ml
+1 -0 metaprl-branches/opname_classes4/theories/itt/itt_record.ml
+2 -2 metaprl-branches/opname_classes4/theories/itt/itt_record.mli
+52 -0 metaprl-branches/opname_classes4/theories/itt/itt_record.prla
+1 -0 metaprl-branches/opname_classes4/theories/itt/itt_record_exm.ml
+72 -20 metaprl-branches/opname_classes4/theories/itt/itt_record_exm.prla
+58 -5 metaprl-branches/opname_classes4/theories/itt/itt_record_label.prla
+12 -10 metaprl-branches/opname_classes4/theories/itt/itt_record_renaming.ml
+1 -0 metaprl-branches/opname_classes4/theories/itt/itt_record_renaming.mli
+55 -3 metaprl-branches/opname_classes4/theories/itt/itt_record_renaming.prla
+1 -3 metaprl-branches/opname_classes4/theories/itt/itt_reflection.prla
+1 -3 metaprl-branches/opname_classes4/theories/itt/itt_reflection_example_lambda.prla
+1 -3 metaprl-branches/opname_classes4/theories/itt/itt_reflection_test.prla
+1 -0 metaprl-branches/opname_classes4/theories/itt/itt_relation_str.ml
+6 -3 metaprl-branches/opname_classes4/theories/itt/itt_ring2.ml
+52 -0 metaprl-branches/opname_classes4/theories/itt/itt_ring2.prla
+1 -0 metaprl-branches/opname_classes4/theories/itt/itt_ring_e.ml
+52 -0 metaprl-branches/opname_classes4/theories/itt/itt_ring_e.prla
+1 -0 metaprl-branches/opname_classes4/theories/itt/itt_ring_uce.ml
+51 -0 metaprl-branches/opname_classes4/theories/itt/itt_ring_uce.prla
+3 -2 metaprl-branches/opname_classes4/theories/itt/itt_set_str.ml
+1 -0 metaprl-branches/opname_classes4/theories/itt/itt_sortedtree.ml
+65 -14 metaprl-branches/opname_classes4/theories/itt/itt_sortedtree.prla
+10 -3 metaprl-branches/opname_classes4/theories/itt/itt_test.ml
+1 -0 metaprl-branches/opname_classes4/theories/itt/itt_unitring.ml
+52 -0 metaprl-branches/opname_classes4/theories/itt/itt_unitring.prla
+2 -15 metaprl-branches/opname_classes4/theories/phobos/phobos_theory.ml
+0 -0 metaprl-branches/opname_classes4/theories/sil/sil_program.ml
+5 -0 metaprl-branches/opname_classes4/theories/sil/sil_programs.ml
+5 -0 metaprl-branches/opname_classes4/theories/sil/sil_programs.mli
+0 -0 metaprl-branches/opname_classes4/theories/sil/sil_sos.ml
+0 -0 metaprl-branches/opname_classes4/theories/sil/sil_state.ml
+1 -0 metaprl-branches/opname_classes4/theories/tptp/tptp.ml
+7001 -8113 metaprl-branches/opname_classes4/theories/tptp/tptp.prla
+1 -0 metaprl-branches/opname_classes4/theories/tptp/tptp_cache.ml
+4 -2 metaprl-branches/opname_classes4/util/gen_refiner_debug.pl
+4 -1 metaprl-branches/opname_classes4/util/gen_refiner_debug_err.pl
Deleted mpcompiler/util/mmc_term_util.ml
Deleted mpcompiler/util/mmc_term_util.mli
+0 -1 mpcompiler-branches/opname_classes4/mmc/OMakefile
+33 -174 mpcompiler-branches/opname_classes4/mmc/arch/x86/mmc_x86_asm.ml
+96 -47 mpcompiler-branches/opname_classes4/mmc/arch/x86/mmc_x86_asm.mli
+95 -90 mpcompiler-branches/opname_classes4/mmc/arch/x86/mmc_x86_backend.ml
+8 -8 mpcompiler-branches/opname_classes4/mmc/arch/x86/mmc_x86_closure.ml
+43 -61 mpcompiler-branches/opname_classes4/mmc/arch/x86/mmc_x86_codegen.ml
+18 -7 mpcompiler-branches/opname_classes4/mmc/arch/x86/mmc_x86_codegen.mli
+56 -56 mpcompiler-branches/opname_classes4/mmc/arch/x86/mmc_x86_convention.ml
+22 -27 mpcompiler-branches/opname_classes4/mmc/arch/x86/mmc_x86_frame.ml
+15 -15 mpcompiler-branches/opname_classes4/mmc/arch/x86/mmc_x86_frame.mli
+1 -1 mpcompiler-branches/opname_classes4/mmc/arch/x86/mmc_x86_hoist.ml
+3 -3 mpcompiler-branches/opname_classes4/mmc/arch/x86/mmc_x86_opt1.ml
+18 -28 mpcompiler-branches/opname_classes4/mmc/arch/x86/mmc_x86_prologue.ml
+16 -9 mpcompiler-branches/opname_classes4/mmc/arch/x86/mmc_x86_prologue.mli
+22 -21 mpcompiler-branches/opname_classes4/mmc/arch/x86/mmc_x86_slop.ml
+59 -57 mpcompiler-branches/opname_classes4/mmc/arch/x86/mmc_x86_spill.ml
+0 -9 mpcompiler-branches/opname_classes4/mmc/base/mmc_base_dform.ml
+1 -1 mpcompiler-branches/opname_classes4/mmc/base/mmc_base_hoist.ml
+1 -1 mpcompiler-branches/opname_classes4/mmc/base/mmc_base_hoist.mli
+0 -23 mpcompiler-branches/opname_classes4/mmc/base/mmc_base_judgment.ml
+39 -4 mpcompiler-branches/opname_classes4/mmc/base/mmc_base_judgment.mli
+0 -7 mpcompiler-branches/opname_classes4/mmc/base/mmc_base_meta.ml
+6 -4 mpcompiler-branches/opname_classes4/mmc/base/mmc_base_meta.mli
+1 -1 mpcompiler-branches/opname_classes4/mmc/base/mmc_base_standardize.ml
+0 -2 mpcompiler-branches/opname_classes4/mmc/core/Files
+12 -70 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_ast.ml
+56 -38 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_ast.mli
+75 -62 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_closure.ml
+0 -4 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_closure.mli
+138 -95 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_cps.ml
+8 -4 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_cps.mli
+11 -18 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_front.ml
+2 -1 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_front.mli
+7 -7 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_grammar.ml
+7 -7 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_grammar.mli
+1 -1 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_hoist.ml
+16 -22 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_inline.ml
+4 -3 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_inline.mli
+2 -1 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_list_util.ml
+2 -1 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_list_util.mli
+4 -4 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_optimize.ml
+18 -27 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_reserve.ml
+5 -8 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_reserve.mli
+95 -32 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_sweep_ty.ml
+3 -0 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_sweep_ty.mli
+16 -46 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_tast.ml
+48 -13 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_tast.mli
+1 -1 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_tast_util.ml
+100 -78 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_type_check.ml
+14 -8 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_type_check.mli
+37 -37 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_type_erase.ml
+12 -1 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_type_erase.mli
+145 -19 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_type_infer.ml
+9 -14 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_value.ml
+6 -4 mpcompiler-branches/opname_classes4/mmc/core/mmc_core_value.mli
+13 -20 mpcompiler-branches/opname_classes4/mmc/extensions/array/mmc_ext_array.ml
+7 -5 mpcompiler-branches/opname_classes4/mmc/extensions/array/mmc_ext_array.mli
+29 -24 mpcompiler-branches/opname_classes4/mmc/extensions/array/mmc_ext_array_x86.ml
+27 -45 mpcompiler-branches/opname_classes4/mmc/extensions/bool/mmc_ext_bool.ml
+21 -15 mpcompiler-branches/opname_classes4/mmc/extensions/bool/mmc_ext_bool.mli
+2 -2 mpcompiler-branches/opname_classes4/mmc/extensions/bool/mmc_ext_boolean_x86.ml
+20 -42 mpcompiler-branches/opname_classes4/mmc/extensions/int/mmc_ext_int.ml
+34 -31 mpcompiler-branches/opname_classes4/mmc/extensions/int/mmc_ext_int.mli
+43 -43 mpcompiler-branches/opname_classes4/mmc/extensions/int/mmc_ext_integer_x86.ml
+7 -10 mpcompiler-branches/opname_classes4/mmc/extensions/loop/mmc_ext_loop.ml
+3 -1 mpcompiler-branches/opname_classes4/mmc/extensions/loop/mmc_ext_loop.mli
+42 -55 mpcompiler-branches/opname_classes4/mmc/extensions/operator/mmc_ext_operator.ml
+43 -7 mpcompiler-branches/opname_classes4/mmc/extensions/operator/mmc_ext_operator.mli
+8 -8 mpcompiler-branches/opname_classes4/mmc/extensions/reserve/mmc_ext_reserve.ml
+1 -1 mpcompiler-branches/opname_classes4/mmc/extensions/reserve/mmc_ext_reserve.mli
+8 -8 mpcompiler-branches/opname_classes4/mmc/extensions/reserve/mmc_ext_reserve_x86.ml
+2 -2 mpcompiler-branches/opname_classes4/mmc/extensions/special/mmc_ext_special.ml
+2 -2 mpcompiler-branches/opname_classes4/mmc/extensions/special/mmc_ext_special.mli
+2 -2 mpcompiler-branches/opname_classes4/mmc/extensions/special/mmc_ext_special_x86.ml
+1 -6 mpcompiler-branches/opname_classes4/mmc/extensions/string/mmc_ext_string.ml
+5 -2 mpcompiler-branches/opname_classes4/mmc/extensions/string/mmc_ext_string.mli
+12 -20 mpcompiler-branches/opname_classes4/mmc/extensions/tuple/mmc_ext_tuple.ml
+7 -5 mpcompiler-branches/opname_classes4/mmc/extensions/tuple/mmc_ext_tuple.mli
+9 -4 mpcompiler-branches/opname_classes4/mmc/extensions/tuple/mmc_ext_tuple_x86.ml
+5 -4 mpcompiler-branches/opname_classes4/mmc/extensions/tyexists/mmc_ext_tyexists.ml
+4 -3 mpcompiler-branches/opname_classes4/mmc/extensions/tyexists/mmc_ext_tyexists.mli
+3 -7 mpcompiler-branches/opname_classes4/mmc/extensions/unit/mmc_ext_unit.ml
+5 -2 mpcompiler-branches/opname_classes4/mmc/extensions/unit/mmc_ext_unit.mli
+0 -1 mpcompiler-branches/opname_classes4/mmc/main/mmc_theory.ml
+0 -1 mpcompiler-branches/opname_classes4/mmc/main/mmc_theory.mli
+37 -37 mpcompiler-branches/opname_classes4/mmc/opt/direct/core/mmc_opt_direct.ml
+23 -23 mpcompiler-branches/opname_classes4/mmc/test/mmc_array_test.ml
+0 -0 mpcompiler-branches/opname_classes4/mmc/test/mmc_core_test.ml
+8 -3 mpcompiler-branches/opname_classes4/mmc/test/mmc_spill_test.ml
+0 -1 mpcompiler-branches/opname_classes4/util/Files
+9 -8 mpcompiler-branches/opname_classes4/util/mm_arith_util.ml
+8 -7 mpcompiler-branches/opname_classes4/util/mm_arith_util.mli
+14 -13 mpcompiler-branches/opname_classes4/util/mm_dform_util.ml
+4 -4 mpcompiler-branches/opname_classes4/util/mm_dform_util.mli
+16 -9 mpcompiler-branches/opname_classes4/util/mm_list_util.ml
+10 -6 mpcompiler-branches/opname_classes4/util/mm_list_util.mli