Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-19 22:24:44 -0800 (Wed, 19 Jan 2005)
Revision: 6451
Log message:

      Merged the opname_classes onto the trank and branched again, creating a fresh
      branch called "opname_classes2".
      

Changes  Path
+54 -52 metaprl-branches/opname_classes2/editor/ml/nuprl_eval.ml
+3 -1 metaprl-branches/opname_classes2/editor/ml/nuprl_jprover.ml
+321 -72 metaprl-branches/opname_classes2/filter/base/filter_cache_fun.ml
+7 -4 metaprl-branches/opname_classes2/filter/base/filter_magic.ml
+418 -46 metaprl-branches/opname_classes2/filter/base/filter_summary.ml
+7 -1 metaprl-branches/opname_classes2/filter/base/filter_summary_type.ml
+32 -4 metaprl-branches/opname_classes2/filter/base/filter_type.ml
+217 -62 metaprl-branches/opname_classes2/filter/filter/filter_parse.ml
+2 -2 metaprl-branches/opname_classes2/filter/filter/filter_patt.ml
+33 -7 metaprl-branches/opname_classes2/filter/filter/filter_prog.ml
+443 -120 metaprl-branches/opname_classes2/filter/filter/term_grammar.ml
+1 -1 metaprl-branches/opname_classes2/filter/phobos/phobos_parser.mly
+29 -26 metaprl-branches/opname_classes2/library/basic.ml
+52 -49 metaprl-branches/opname_classes2/library/db.ml
+17 -15 metaprl-branches/opname_classes2/library/definition.ml
+9 -7 metaprl-branches/opname_classes2/library/library.ml
+5 -3 metaprl-branches/opname_classes2/library/link.ml
+6 -4 metaprl-branches/opname_classes2/library/mbterm.ml
+58 -36 metaprl-branches/opname_classes2/library/nuprl5.ml
+40 -38 metaprl-branches/opname_classes2/library/orb.ml
+14 -0 metaprl-branches/opname_classes2/refiner/refbase/opname.ml
+9 -1 metaprl-branches/opname_classes2/refiner/refbase/opname.mli
+2 -2 metaprl-branches/opname_classes2/refiner/refiner/refine.ml
+2 -2 metaprl-branches/opname_classes2/refiner/refiner/refine.mli
+15 -11 metaprl-branches/opname_classes2/refiner/refiner/refine_error.ml
+4 -4 metaprl-branches/opname_classes2/refiner/refiner/refine_error.mli
+9 -1 metaprl-branches/opname_classes2/refiner/refiner/refiner_ds.ml
+9 -2 metaprl-branches/opname_classes2/refiner/refiner/refiner_std.ml
+1 -0 metaprl-branches/opname_classes2/refiner/reflib/Files
+17 -11 metaprl-branches/opname_classes2/refiner/reflib/ascii_io.ml
+6 -1 metaprl-branches/opname_classes2/refiner/reflib/dform.ml
+165 -124 metaprl-branches/opname_classes2/refiner/reflib/refine_exn.ml
+1 -1 metaprl-branches/opname_classes2/refiner/reflib/simple_print.ml
Added metaprl-branches/opname_classes2/refiner/reflib/term_class_infer.ml
Properties metaprl-branches/opname_classes2/refiner/reflib/term_class_infer.ml
Added metaprl-branches/opname_classes2/refiner/reflib/term_class_infer.mli
Properties metaprl-branches/opname_classes2/refiner/reflib/term_class_infer.mli
+35 -19 metaprl-branches/opname_classes2/refiner/reflib/term_match_table.ml
+4 -0 metaprl-branches/opname_classes2/refiner/reflib/term_match_table.mli
+124 -124 metaprl-branches/opname_classes2/refiner/reflib/term_order.ml
+1 -0 metaprl-branches/opname_classes2/refiner/refsig/Files
+18 -8 metaprl-branches/opname_classes2/refiner/refsig/refine_error_sig.ml
+8 -2 metaprl-branches/opname_classes2/refiner/refsig/refiner_sig.ml
+3 -0 metaprl-branches/opname_classes2/refiner/refsig/rewrite_sig.ml
Added metaprl-branches/opname_classes2/refiner/refsig/term_class_sig.ml
Properties metaprl-branches/opname_classes2/refiner/refsig/term_class_sig.ml
+4 -4 metaprl-branches/opname_classes2/refiner/refsig/term_op_sig.ml
+3 -0 metaprl-branches/opname_classes2/refiner/refsig/term_shape_sig.ml
+2 -2 metaprl-branches/opname_classes2/refiner/refsig/term_sig.ml
+2 -0 metaprl-branches/opname_classes2/refiner/refsig/term_subst_sig.ml
+27 -14 metaprl-branches/opname_classes2/refiner/rewrite/rewrite.ml
+1 -1 metaprl-branches/opname_classes2/refiner/rewrite/rewrite.mli
+2 -2 metaprl-branches/opname_classes2/refiner/rewrite/rewrite_build_contractum.ml
+1 -1 metaprl-branches/opname_classes2/refiner/rewrite/rewrite_build_contractum.mli
+1 -1 metaprl-branches/opname_classes2/refiner/rewrite/rewrite_compile_contractum.ml
+1 -1 metaprl-branches/opname_classes2/refiner/rewrite/rewrite_compile_contractum.mli
+14 -14 metaprl-branches/opname_classes2/refiner/rewrite/rewrite_compile_redex.ml
+1 -1 metaprl-branches/opname_classes2/refiner/rewrite/rewrite_compile_redex.mli
+5 -3 metaprl-branches/opname_classes2/refiner/rewrite/rewrite_debug.ml
+1 -1 metaprl-branches/opname_classes2/refiner/rewrite/rewrite_debug.mli
+5 -4 metaprl-branches/opname_classes2/refiner/rewrite/rewrite_match_redex.ml
+1 -1 metaprl-branches/opname_classes2/refiner/rewrite/rewrite_match_redex.mli
+6 -4 metaprl-branches/opname_classes2/refiner/rewrite/rewrite_meta.ml
+1 -1 metaprl-branches/opname_classes2/refiner/rewrite/rewrite_meta.mli
+2 -1 metaprl-branches/opname_classes2/refiner/rewrite/rewrite_types.ml
+1 -1 metaprl-branches/opname_classes2/refiner/rewrite/rewrite_util.ml
+1 -1 metaprl-branches/opname_classes2/refiner/rewrite/rewrite_util.mli
+2 -2 metaprl-branches/opname_classes2/refiner/term_ds/term_addr_ds.ml
+2 -2 metaprl-branches/opname_classes2/refiner/term_ds/term_addr_ds.mli
+4 -4 metaprl-branches/opname_classes2/refiner/term_ds/term_base_ds.ml
+4 -4 metaprl-branches/opname_classes2/refiner/term_ds/term_base_ds.mli
+1 -1 metaprl-branches/opname_classes2/refiner/term_ds/term_ds.ml
+1 -1 metaprl-branches/opname_classes2/refiner/term_ds/term_ds_sig.ml
+4 -4 metaprl-branches/opname_classes2/refiner/term_ds/term_eval_ds.ml
+4 -4 metaprl-branches/opname_classes2/refiner/term_ds/term_eval_ds.mli
+2 -2 metaprl-branches/opname_classes2/refiner/term_ds/term_man_ds.ml
+2 -2 metaprl-branches/opname_classes2/refiner/term_ds/term_man_ds.mli
+4 -4 metaprl-branches/opname_classes2/refiner/term_ds/term_op_ds.ml
+6 -5 metaprl-branches/opname_classes2/refiner/term_ds/term_op_ds.mli
+38 -4 metaprl-branches/opname_classes2/refiner/term_ds/term_subst_ds.ml
+6 -5 metaprl-branches/opname_classes2/refiner/term_ds/term_subst_ds.mli
+1 -0 metaprl-branches/opname_classes2/refiner/term_gen/Files
+2 -2 metaprl-branches/opname_classes2/refiner/term_gen/term_addr_gen.ml
+2 -2 metaprl-branches/opname_classes2/refiner/term_gen/term_addr_gen.mli
Added metaprl-branches/opname_classes2/refiner/term_gen/term_class_gen.ml
Properties metaprl-branches/opname_classes2/refiner/term_gen/term_class_gen.ml
Added metaprl-branches/opname_classes2/refiner/term_gen/term_class_gen.mli
Properties metaprl-branches/opname_classes2/refiner/term_gen/term_class_gen.mli
+1 -1 metaprl-branches/opname_classes2/refiner/term_gen/term_man_gen.ml
+1 -1 metaprl-branches/opname_classes2/refiner/term_gen/term_man_gen.mli
+1 -1 metaprl-branches/opname_classes2/refiner/term_gen/term_meta_gen.ml
+1 -1 metaprl-branches/opname_classes2/refiner/term_gen/term_meta_gen.mli
+32 -5 metaprl-branches/opname_classes2/refiner/term_gen/term_shape_gen.ml
+7 -0 metaprl-branches/opname_classes2/refiner/term_gen/term_shape_gen.mli
+1 -1 metaprl-branches/opname_classes2/refiner/term_std/term_base_std.ml
+1 -1 metaprl-branches/opname_classes2/refiner/term_std/term_base_std.mli
+1 -1 metaprl-branches/opname_classes2/refiner/term_std/term_eval_std.ml
+1 -1 metaprl-branches/opname_classes2/refiner/term_std/term_eval_std.mli
+1 -1 metaprl-branches/opname_classes2/refiner/term_std/term_op_std.ml
+1 -1 metaprl-branches/opname_classes2/refiner/term_std/term_op_std.mli
+1 -1 metaprl-branches/opname_classes2/refiner/term_std/term_std.ml
+1 -1 metaprl-branches/opname_classes2/refiner/term_std/term_std_sig.ml
+25 -2 metaprl-branches/opname_classes2/refiner/term_std/term_subst_std.ml
+1 -1 metaprl-branches/opname_classes2/refiner/term_std/term_subst_std.mli
+32 -0 metaprl-branches/opname_classes2/support/display/summary.ml
+7 -0 metaprl-branches/opname_classes2/support/shell/package_info.ml
+1 -0 metaprl-branches/opname_classes2/support/shell/package_info.mli
+8 -1 metaprl-branches/opname_classes2/support/shell/shell_core.ml
+5 -1 metaprl-branches/opname_classes2/support/shell/shell_package.ml
+19 -0 metaprl-branches/opname_classes2/support/shell/shell_state.ml
+2 -0 metaprl-branches/opname_classes2/support/shell/shell_state.mli
+4 -6 metaprl-branches/opname_classes2/support/tactics/dtactic.ml
+2 -2 metaprl-branches/opname_classes2/theories/czf/czf_itt_equiv.ml
+3 -9 metaprl-branches/opname_classes2/theories/czf/czf_itt_equiv.mli
+1 -5 metaprl-branches/opname_classes2/theories/czf/czf_itt_sall.mli
+1 -5 metaprl-branches/opname_classes2/theories/czf/czf_itt_sexists.mli
+3 -3 metaprl-branches/opname_classes2/theories/experimental/compile/m_ast.ml
+1 -1 metaprl-branches/opname_classes2/theories/experimental/compile/m_ast.mli
+4 -4 metaprl-branches/opname_classes2/theories/experimental/compile/m_cps.ml
+1 -1 metaprl-branches/opname_classes2/theories/experimental/compile/m_doc_ir.ml
+1 -1 metaprl-branches/opname_classes2/theories/experimental/compile/m_doc_ir.mli
+2 -2 metaprl-branches/opname_classes2/theories/experimental/compile/m_doc_proposal.ml
+1 -1 metaprl-branches/opname_classes2/theories/experimental/compile/m_doc_proposal.mli
+3 -3 metaprl-branches/opname_classes2/theories/experimental/compile/m_ir.ml
+1 -1 metaprl-branches/opname_classes2/theories/experimental/compile/m_ir.mli
+5 -5 metaprl-branches/opname_classes2/theories/experimental/compile/m_ir_ast.ml
+10 -8 metaprl-branches/opname_classes2/theories/experimental/compile/m_test.ml
+12 -12 metaprl-branches/opname_classes2/theories/experimental/compile/m_x86_asm.ml
+4 -4 metaprl-branches/opname_classes2/theories/experimental/compile/m_x86_asm.mli
+12 -12 metaprl-branches/opname_classes2/theories/experimental/compile/m_x86_codegen.ml
+11 -11 metaprl-branches/opname_classes2/theories/experimental/compile/m_x86_term.ml
Properties metaprl-branches/opname_classes2/theories/experimental/syntax
Added metaprl-branches/opname_classes2/theories/experimental/syntax/OMakefile
Properties metaprl-branches/opname_classes2/theories/experimental/syntax/OMakefile
Added metaprl-branches/opname_classes2/theories/experimental/syntax/syntax_test.ml
Properties metaprl-branches/opname_classes2/theories/experimental/syntax/syntax_test.ml
Added metaprl-branches/opname_classes2/theories/experimental/syntax/syntax_test.mli
Properties metaprl-branches/opname_classes2/theories/experimental/syntax/syntax_test.mli
+2 -0 metaprl-branches/opname_classes2/theories/itt/OMakefile
+1 -2 metaprl-branches/opname_classes2/theories/itt/itt_algebra_df.ml
+1 -5 metaprl-branches/opname_classes2/theories/itt/itt_atom.ml
+2 -2 metaprl-branches/opname_classes2/theories/itt/itt_atom.mli
+4 -3 metaprl-branches/opname_classes2/theories/itt/itt_grouplikeobj.ml
+2 -2 metaprl-branches/opname_classes2/theories/itt/itt_record.mli
+5 -3 metaprl-branches/opname_classes2/theories/itt/itt_ring2.ml
+1 -0 metaprl-branches/opname_classes2/theories/tptp/tptp.ml
+3 -0 metaprl-branches/opname_classes2/util/check-status.sh