Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-14 21:12:36 -0800 (Sat, 14 Jan 2006)
Revision: 8482
Log message:

      Merged in the trunk changes (revisions 8281:8481):
         svn merge -r 8281:8481 svn+ssh://svn.metaprl.org/svnroot/mojave/metaprl
      

Changes  Path
+21 -13 metaprl-branches/new_binary_io/OMakefile
+1 -1 metaprl-branches/new_binary_io/doc/latex/theories/OMakefile
Properties metaprl-branches/new_binary_io/editor/ml
+24 -3 metaprl-branches/new_binary_io/editor/ml/OMakefile
+11 -1 metaprl-branches/new_binary_io/editor/ml/make_mp_version.ml
+1 -1 metaprl-branches/new_binary_io/editor/ml/mpxterm
+2 -0 metaprl-branches/new_binary_io/filter/OMakefile
+1 -0 metaprl-branches/new_binary_io/filter/base/Files
+1 -0 metaprl-branches/new_binary_io/filter/base/OMakefile
+38 -28 metaprl-branches/new_binary_io/filter/base/filter_cache_fun.ml
+1 -23 metaprl-branches/new_binary_io/filter/base/filter_exn.ml
+34 -2 metaprl-branches/new_binary_io/filter/base/filter_grammar.ml
+4 -3 metaprl-branches/new_binary_io/filter/base/filter_io.ml
+532 -235 metaprl-branches/new_binary_io/filter/base/filter_reflection.ml
+24 -15 metaprl-branches/new_binary_io/filter/base/filter_reflection.mli
Copied metaprl-branches/new_binary_io/filter/base/filter_shape.ml
Properties metaprl-branches/new_binary_io/filter/base/filter_shape.ml
Copied metaprl-branches/new_binary_io/filter/base/filter_shape.mli
Properties metaprl-branches/new_binary_io/filter/base/filter_shape.mli
+63 -44 metaprl-branches/new_binary_io/filter/base/filter_summary.ml
+0 -3 metaprl-branches/new_binary_io/filter/base/filter_summary.mli
+1 -1 metaprl-branches/new_binary_io/filter/base/filter_summary_type.ml
+10 -13 metaprl-branches/new_binary_io/filter/base/filter_type.ml
+3 -3 metaprl-branches/new_binary_io/filter/base/filter_util.ml
+1 -1 metaprl-branches/new_binary_io/filter/base/filter_util.mli
+2 -1 metaprl-branches/new_binary_io/filter/filter/filter_main.ml
+158 -160 metaprl-branches/new_binary_io/filter/filter/filter_parse.ml
+32 -9 metaprl-branches/new_binary_io/filter/filter/filter_prog.ml
+1 -0 metaprl-branches/new_binary_io/filter/filter/filter_prog.mli
+26 -22 metaprl-branches/new_binary_io/filter/filter/term_grammar.ml
+8 -0 metaprl-branches/new_binary_io/lib/words
+2 -1 metaprl-branches/new_binary_io/mk/defaults
+10 -0 metaprl-branches/new_binary_io/mk/make_config
+10 -2 metaprl-branches/new_binary_io/mk/prlcomp
+1 -0 metaprl-branches/new_binary_io/mllib/OMakefile
+0 -36 metaprl-branches/new_binary_io/mllib/comment_parse.mll
+63 -64 metaprl-branches/new_binary_io/mllib/weak_memo.ml
+0 -5 metaprl-branches/new_binary_io/mllib/weak_memo_sig.ml
+38 -10 metaprl-branches/new_binary_io/refiner/refiner/refine.ml
+1 -0 metaprl-branches/new_binary_io/refiner/refiner/refine_error.ml
+52 -16 metaprl-branches/new_binary_io/refiner/refiner/refiner_debug.ml
+1 -0 metaprl-branches/new_binary_io/refiner/reflib/OMakefile
+3 -3 metaprl-branches/new_binary_io/refiner/reflib/match_seq.ml
+6 -3 metaprl-branches/new_binary_io/refiner/reflib/match_seq.mli
+3 -1 metaprl-branches/new_binary_io/refiner/reflib/mp_resource.ml
+2 -0 metaprl-branches/new_binary_io/refiner/reflib/mp_resource.mli
+3 -0 metaprl-branches/new_binary_io/refiner/reflib/refine_exn.ml
+28 -0 metaprl-branches/new_binary_io/refiner/reflib/simple_print.ml
+5 -0 metaprl-branches/new_binary_io/refiner/reflib/simple_print.mli
+8 -6 metaprl-branches/new_binary_io/refiner/reflib/term_hash_code.ml
+0 -0 metaprl-branches/new_binary_io/refiner/reflib/term_match_table.ml
+1 -1 metaprl-branches/new_binary_io/refiner/reflib/term_match_table.mli
+1 -1 metaprl-branches/new_binary_io/refiner/reflib/term_order.mli
+1 -0 metaprl-branches/new_binary_io/refiner/refsig/refine_error_sig.ml
+7 -4 metaprl-branches/new_binary_io/refiner/refsig/refine_sig.ml
+0 -6 metaprl-branches/new_binary_io/refiner/refsig/term_hash_sig.ml
+5 -0 metaprl-branches/new_binary_io/refiner/refsig/term_man_sig.ml
+1 -0 metaprl-branches/new_binary_io/refiner/refsig/term_shape_sig.ml
+2 -0 metaprl-branches/new_binary_io/refiner/refsig/thread_refiner_sig.ml
+57 -18 metaprl-branches/new_binary_io/refiner/term_ds/term_man_ds.ml
+12 -16 metaprl-branches/new_binary_io/refiner/term_gen/term_hash.ml
+10 -0 metaprl-branches/new_binary_io/refiner/term_gen/term_man_gen.ml
+1 -0 metaprl-branches/new_binary_io/refiner/term_gen/term_shape_gen.ml
+1 -1 metaprl-branches/new_binary_io/refiner/term_std/term_subst_std.ml
+1 -1 metaprl-branches/new_binary_io/support/display/perv.mli
+9 -0 metaprl-branches/new_binary_io/support/display/summary.ml
+4 -0 metaprl-branches/new_binary_io/support/shell/OMakefile
+15 -7 metaprl-branches/new_binary_io/support/shell/proof_edit.ml
+0 -1 metaprl-branches/new_binary_io/support/shell/proof_edit.mli
+16 -17 metaprl-branches/new_binary_io/support/shell/shell_package.ml
+2 -2 metaprl-branches/new_binary_io/support/shell/shell_rule.ml
+15 -2 metaprl-branches/new_binary_io/support/shell/shell_state.ml
+1 -0 metaprl-branches/new_binary_io/support/tactics/OMakefile
+74 -36 metaprl-branches/new_binary_io/support/tactics/auto_tactic.ml
+10 -7 metaprl-branches/new_binary_io/support/tactics/auto_tactic.mli
+2 -0 metaprl-branches/new_binary_io/support/tactics/basic_tactics.ml
+10 -7 metaprl-branches/new_binary_io/support/tactics/dtactic.ml
Copied metaprl-branches/new_binary_io/support/tactics/forward.ml
Properties metaprl-branches/new_binary_io/support/tactics/forward.ml
Copied metaprl-branches/new_binary_io/support/tactics/forward.mli
Properties metaprl-branches/new_binary_io/support/tactics/forward.mli
+40 -3 metaprl-branches/new_binary_io/support/tactics/top_conversionals.ml
+5 -2 metaprl-branches/new_binary_io/support/tactics/top_tacticals.ml
+2 -1 metaprl-branches/new_binary_io/support/tactics/top_tacticals.mli
+4 -0 metaprl-branches/new_binary_io/tactics/null/thread_refiner.ml
+46 -12 metaprl-branches/new_binary_io/tactics/proof/proof_boot.ml
+1 -2 metaprl-branches/new_binary_io/tactics/proof/proof_term_boot.ml
+2 -2 metaprl-branches/new_binary_io/tactics/proof/rewrite_boot.ml
+1 -0 metaprl-branches/new_binary_io/tactics/proof/sequent_boot.ml
+37 -18 metaprl-branches/new_binary_io/tactics/proof/tactic_boot.ml
+15 -2 metaprl-branches/new_binary_io/tactics/proof/tactic_boot_sig.ml
+79 -76 metaprl-branches/new_binary_io/tactics/proof/tacticals_boot.ml
+1 -1 metaprl-branches/new_binary_io/theories/fol/fol_struct.ml
+2 -0 metaprl-branches/new_binary_io/theories/itt/applications/OMakefile
+1 -1 metaprl-branches/new_binary_io/theories/itt/applications/function_spaces/itt_closure.ml
+2 -2 metaprl-branches/new_binary_io/theories/itt/applications/function_spaces/itt_closure.prla
+8 -8 metaprl-branches/new_binary_io/theories/itt/applications/function_spaces/itt_functions.ml
+2 -3 metaprl-branches/new_binary_io/theories/itt/applications/function_spaces/itt_functions.prla
+5 -0 metaprl-branches/new_binary_io/theories/itt/applications/objects/OMakefile
Copied metaprl-branches/new_binary_io/theories/itt/applications/objects/itt_closed_intsect.ml
Copied metaprl-branches/new_binary_io/theories/itt/applications/objects/itt_closed_intsect.mli
Copied metaprl-branches/new_binary_io/theories/itt/applications/objects/itt_monotone_subtyping.ml
Copied metaprl-branches/new_binary_io/theories/itt/applications/objects/itt_monotone_subtyping.mli
Copied metaprl-branches/new_binary_io/theories/itt/applications/objects/itt_monotone_subtyping.prla
Copied metaprl-branches/new_binary_io/theories/itt/applications/objects/itt_obj_base_closetype.ml
Copied metaprl-branches/new_binary_io/theories/itt/applications/objects/itt_obj_base_closetype.mli
Copied metaprl-branches/new_binary_io/theories/itt/applications/objects/itt_obj_base_exttype.ml
Copied metaprl-branches/new_binary_io/theories/itt/applications/objects/itt_obj_base_exttype.mli
+5 -0 metaprl-branches/new_binary_io/theories/itt/applications/objects/itt_obj_base_rewrite.mli
Copied metaprl-branches/new_binary_io/theories/itt/applications/objects/itt_union_of.ml
Copied metaprl-branches/new_binary_io/theories/itt/applications/objects/itt_union_of.mli
+1 -0 metaprl-branches/new_binary_io/theories/itt/core/OMakefile
+1 -1 metaprl-branches/new_binary_io/theories/itt/core/itt_atom.ml
+1 -1 metaprl-branches/new_binary_io/theories/itt/core/itt_atom.mli
+18 -13 metaprl-branches/new_binary_io/theories/itt/core/itt_atom_bool.ml
Copied metaprl-branches/new_binary_io/theories/itt/core/itt_atom_bool.prla
Properties metaprl-branches/new_binary_io/theories/itt/core/itt_atom_bool.prla
+18 -12 metaprl-branches/new_binary_io/theories/itt/core/itt_bool.ml
+8 -3 metaprl-branches/new_binary_io/theories/itt/core/itt_bool.mli
+5422 -5392 metaprl-branches/new_binary_io/theories/itt/core/itt_bool.prla
+2 -0 metaprl-branches/new_binary_io/theories/itt/core/itt_equal.mli
+454 -474 metaprl-branches/new_binary_io/theories/itt/core/itt_int_arith.ml
+6 -7 metaprl-branches/new_binary_io/theories/itt/core/itt_int_arith.mli
+18744 -18563 metaprl-branches/new_binary_io/theories/itt/core/itt_int_arith.prla
+32 -13 metaprl-branches/new_binary_io/theories/itt/core/itt_int_base.ml
+1 -1 metaprl-branches/new_binary_io/theories/itt/core/itt_int_base.mli
+7422 -6570 metaprl-branches/new_binary_io/theories/itt/core/itt_int_base.prla
+9 -5 metaprl-branches/new_binary_io/theories/itt/core/itt_int_ext.ml
+1 -1 metaprl-branches/new_binary_io/theories/itt/core/itt_isect.ml
+1 -1 metaprl-branches/new_binary_io/theories/itt/core/itt_isect.mli
+0 -0 metaprl-branches/new_binary_io/theories/itt/core/itt_list.ml
+91 -31 metaprl-branches/new_binary_io/theories/itt/core/itt_list2.ml
+4 -1 metaprl-branches/new_binary_io/theories/itt/core/itt_list2.mli
+33190 -24492 metaprl-branches/new_binary_io/theories/itt/core/itt_list2.prla
Copied metaprl-branches/new_binary_io/theories/itt/core/itt_list_set.ml
Properties metaprl-branches/new_binary_io/theories/itt/core/itt_list_set.ml
Copied metaprl-branches/new_binary_io/theories/itt/core/itt_list_set.mli
Properties metaprl-branches/new_binary_io/theories/itt/core/itt_list_set.mli
Copied metaprl-branches/new_binary_io/theories/itt/core/itt_list_set.prla
Properties metaprl-branches/new_binary_io/theories/itt/core/itt_list_set.prla
+10 -1 metaprl-branches/new_binary_io/theories/itt/core/itt_logic.ml
+3 -1 metaprl-branches/new_binary_io/theories/itt/core/itt_logic.mli
+28463 -29860 metaprl-branches/new_binary_io/theories/itt/core/itt_logic.prla
+35 -11 metaprl-branches/new_binary_io/theories/itt/core/itt_nat.ml
+2 -1 metaprl-branches/new_binary_io/theories/itt/core/itt_nat.mli
+7657 -6365 metaprl-branches/new_binary_io/theories/itt/core/itt_nat.prla
+71 -32 metaprl-branches/new_binary_io/theories/itt/core/itt_omega.ml
+26 -0 metaprl-branches/new_binary_io/theories/itt/core/itt_omega.mli
+44594 -42815 metaprl-branches/new_binary_io/theories/itt/core/itt_omega.prla
+1212 -1220 metaprl-branches/new_binary_io/theories/itt/core/itt_record0.prla
+54 -22 metaprl-branches/new_binary_io/theories/itt/core/itt_sqsimple.ml
+10 -7 metaprl-branches/new_binary_io/theories/itt/core/itt_sqsimple.mli
+3474 -2282 metaprl-branches/new_binary_io/theories/itt/core/itt_sqsimple.prla
+5 -3 metaprl-branches/new_binary_io/theories/itt/core/itt_squash.ml
+2 -0 metaprl-branches/new_binary_io/theories/itt/core/itt_squiggle.ml
+131 -9 metaprl-branches/new_binary_io/theories/itt/core/itt_struct.ml
+7 -1 metaprl-branches/new_binary_io/theories/itt/core/itt_struct.mli
+11737 -7915 metaprl-branches/new_binary_io/theories/itt/core/itt_struct.prla
+192 -83 metaprl-branches/new_binary_io/theories/itt/core/itt_struct2.ml
+10 -8 metaprl-branches/new_binary_io/theories/itt/core/itt_struct2.mli
+10634 -8570 metaprl-branches/new_binary_io/theories/itt/core/itt_struct2.prla
+1 -0 metaprl-branches/new_binary_io/theories/itt/core/itt_theory.ml
+1 -1 metaprl-branches/new_binary_io/theories/itt/core/itt_unit.ml
+1 -1 metaprl-branches/new_binary_io/theories/itt/core/itt_unit.mli
+1 -1 metaprl-branches/new_binary_io/theories/itt/core/itt_void.ml
+1 -1 metaprl-branches/new_binary_io/theories/itt/core/itt_void.mli
+2 -0 metaprl-branches/new_binary_io/theories/itt/extensions/OMakefile
+1 -0 metaprl-branches/new_binary_io/theories/itt/extensions/base/OMakefile
+101 -308 metaprl-branches/new_binary_io/theories/itt/extensions/base/itt_list3.ml
+5 -23 metaprl-branches/new_binary_io/theories/itt/extensions/base/itt_list3.mli
+3670 -10630 metaprl-branches/new_binary_io/theories/itt/extensions/base/itt_list3.prla
Copied metaprl-branches/new_binary_io/theories/itt/extensions/base/itt_list_sloppy.ml
Properties metaprl-branches/new_binary_io/theories/itt/extensions/base/itt_list_sloppy.ml
Copied metaprl-branches/new_binary_io/theories/itt/extensions/base/itt_list_sloppy.mli
Properties metaprl-branches/new_binary_io/theories/itt/extensions/base/itt_list_sloppy.mli
Copied metaprl-branches/new_binary_io/theories/itt/extensions/base/itt_list_sloppy.prla
Properties metaprl-branches/new_binary_io/theories/itt/extensions/base/itt_list_sloppy.prla
+21 -47 metaprl-branches/new_binary_io/theories/itt/extensions/base/pairwise-verification.ml
Properties metaprl-branches/new_binary_io/theories/itt/extensions/vector
+7 -15 metaprl-branches/new_binary_io/theories/itt/extensions/vector/itt_vec_bind.ml
+0 -1 metaprl-branches/new_binary_io/theories/itt/extensions/vector/itt_vec_bind.mli
+2231 -2189 metaprl-branches/new_binary_io/theories/itt/extensions/vector/itt_vec_bind.prla
+418 -33 metaprl-branches/new_binary_io/theories/itt/extensions/vector/itt_vec_list1.ml
+15 -2 metaprl-branches/new_binary_io/theories/itt/extensions/vector/itt_vec_list1.mli
+7810 -834 metaprl-branches/new_binary_io/theories/itt/extensions/vector/itt_vec_list1.prla
+45 -18 metaprl-branches/new_binary_io/theories/itt/extensions/vector/itt_vec_sequent_term.ml
+13 -0 metaprl-branches/new_binary_io/theories/itt/extensions/vector/itt_vec_sequent_term.mli
+5998 -5859 metaprl-branches/new_binary_io/theories/itt/extensions/vector/itt_vec_sequent_term.prla
+1 -1 metaprl-branches/new_binary_io/theories/itt/extensions/vector/itt_vec_struct.ml
Deleted metaprl-branches/new_binary_io/theories/itt/extensions/vector/itt_vec_theory.ml
Deleted metaprl-branches/new_binary_io/theories/itt/extensions/vector/itt_vec_theory.mli
+2 -0 metaprl-branches/new_binary_io/theories/itt/reflection/OMakefile
+1 -0 metaprl-branches/new_binary_io/theories/itt/reflection/core/OMakefile
+36 -0 metaprl-branches/new_binary_io/theories/itt/reflection/core/itt_hoas_base.ml
+13 -0 metaprl-branches/new_binary_io/theories/itt/reflection/core/itt_hoas_base.mli
+3516 -2293 metaprl-branches/new_binary_io/theories/itt/reflection/core/itt_hoas_base.prla
+54 -5 metaprl-branches/new_binary_io/theories/itt/reflection/core/itt_hoas_debruijn.ml
+21 -0 metaprl-branches/new_binary_io/theories/itt/reflection/core/itt_hoas_debruijn.mli
+4221 -2406 metaprl-branches/new_binary_io/theories/itt/reflection/core/itt_hoas_debruijn.prla
+4 -0 metaprl-branches/new_binary_io/theories/itt/reflection/core/itt_hoas_operator.ml
+2603 -1670 metaprl-branches/new_binary_io/theories/itt/reflection/core/itt_hoas_operator.prla
+83 -1 metaprl-branches/new_binary_io/theories/itt/reflection/core/itt_hoas_vbind.ml
+2 -0 metaprl-branches/new_binary_io/theories/itt/reflection/core/itt_hoas_vbind.mli
+1998 -604 metaprl-branches/new_binary_io/theories/itt/reflection/core/itt_hoas_vbind.prla
+91 -2 metaprl-branches/new_binary_io/theories/itt/reflection/core/itt_hoas_vector.ml
+21 -0 metaprl-branches/new_binary_io/theories/itt/reflection/core/itt_hoas_vector.mli
+5500 -4265 metaprl-branches/new_binary_io/theories/itt/reflection/core/itt_hoas_vector.prla
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental
+15 -2 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/OMakefile
+55 -18 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_bterm.ml
+4 -1 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_bterm.mli
+8848 -7983 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_bterm.prla
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_bterm_wf.ml
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_bterm_wf.ml
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_bterm_wf.mli
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_bterm_wf.mli
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_bterm_wf.prla
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_bterm_wf.prla
+2580 -2840 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_lang.prla
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_lof.ml
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_lof.ml
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_lof.mli
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_lof.mli
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_lof.prla
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_lof.prla
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_lof_vec.ml
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_lof_vec.ml
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_lof_vec.mli
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_lof_vec.mli
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_lof_vec.prla
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_lof_vec.prla
+12 -3 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_meta_types.ml
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_normalize.ml
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_normalize.ml
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_normalize.mli
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_normalize.mli
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_normalize.prla
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_normalize.prla
+128 -4 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_proof.ml
+32 -1 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_proof.mli
+9174 -11262 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_proof.prla
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_proof1.ml
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_proof1.ml
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_proof1.mli
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_proof1.mli
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_proof1.prla
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_proof1.prla
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_proof_ind.ml
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_proof_ind.mli
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_proof_ind.prla
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_relax.ml
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_relax.ml
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_relax.mli
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_relax.mli
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_relax.prla
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_relax.prla
+208 -19 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent.ml
+9 -3 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent.mli
+9191 -4175 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent.prla
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_bterm.ml
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_bterm.ml
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_bterm.mli
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_bterm.mli
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_bterm.prla
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_bterm.prla
Deleted metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_proof.ml
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_proof.ml
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_proof.ml
Deleted metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_proof.mli
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_proof.mli
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_proof.mli
Deleted metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_proof.prla
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_proof.prla
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_proof.prla
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_proof1.ml
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_proof1.ml
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_proof1.mli
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_proof1.mli
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_proof1.prla
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_proof1.prla
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_proof_step.ml
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_proof_step.ml
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_proof_step.mli
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_proof_step.mli
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_proof_step.prla
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_proof_step.prla
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_proof_step1.ml
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_proof_step1.ml
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_proof_step1.mli
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_proof_step1.mli
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_proof_step1.prla
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_proof_step1.prla
Deleted metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_provable.ml
Deleted metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_provable.mli
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_term.ml
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_term.ml
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_term.mli
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_term.mli
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_term.prla
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_term.prla
+284 -12 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_term1.ml
+19 -3 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_term1.mli
+6637 -4438 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_term1.prla
Deleted metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_theory.ml
Deleted metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_theory.mli
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_theory.mlz
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_theory.mlz
+25 -30 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_util.ml
+6 -14 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_util.mli
+7 -0 metaprl-branches/new_binary_io/theories/itt/tests/itt_int_test.ml
+2605 -2335 metaprl-branches/new_binary_io/theories/itt/tests/itt_int_test.prla
Properties metaprl-branches/new_binary_io/theories/meta
+1 -1 metaprl-branches/new_binary_io/theories/meta/OMakefile
+20 -9 metaprl-branches/new_binary_io/theories/meta/base/base_grammar.mli
+1 -0 metaprl-branches/new_binary_io/theories/meta/base/base_theory.mlz
+6 -1 metaprl-branches/new_binary_io/theories/meta/base/base_trivial.ml
+4 -1 metaprl-branches/new_binary_io/theories/meta/base/base_trivial.mli
Properties metaprl-branches/new_binary_io/theories/meta/extensions
+2 -2 metaprl-branches/new_binary_io/theories/meta/extensions/OMakefile
+16 -8 metaprl-branches/new_binary_io/theories/meta/extensions/meta_context_ind1.ml
+4 -4 metaprl-branches/new_binary_io/theories/meta/extensions/meta_context_terms.ml
+1 -1 metaprl-branches/new_binary_io/theories/meta/extensions/meta_context_terms.mli
+10 -10 metaprl-branches/new_binary_io/theories/meta/extensions/meta_context_terms2.ml
+2 -2 metaprl-branches/new_binary_io/theories/meta/extensions/meta_context_terms2.prla
Copied metaprl-branches/new_binary_io/theories/meta/extensions/meta_context_theory.mlz
Properties metaprl-branches/new_binary_io/theories/meta/extensions/meta_context_theory.mlz
+6 -4 metaprl-branches/new_binary_io/theories/meta/extensions/meta_dtactic.ml
Deleted metaprl-branches/new_binary_io/theories/meta/extensions/meta_extensions_theory.ml
Deleted metaprl-branches/new_binary_io/theories/meta/extensions/meta_extensions_theory.mli
Deleted metaprl-branches/new_binary_io/theories/meta/extensions/meta_extensions_theory.mlz
+2 -2 metaprl-branches/new_binary_io/theories/ocaml_doc/ocaml_doc_class2.ml
+1 -1 metaprl-branches/new_binary_io/theories/ocaml_doc/ocaml_doc_exn1.ml
+1 -1 metaprl-branches/new_binary_io/theories/ocaml_doc/ocaml_doc_mod2.ml
+1 -1 metaprl-branches/new_binary_io/theories/ocaml_doc/ocaml_doc_mod3.ml
+5 -2 metaprl-branches/new_binary_io/theories/poplmark/naive/OMakefile
+47 -7 metaprl-branches/new_binary_io/theories/poplmark/naive/pmn_core_terms.ml
+0 -4 metaprl-branches/new_binary_io/theories/poplmark/naive/pmn_core_terms.mli
Deleted metaprl-branches/new_binary_io/theories/poplmark/naive/pmn_core_terms.prla
+0 -6 metaprl-branches/new_binary_io/util/OMakefile
+13 -7 metaprl-branches/new_binary_io/util/check-status.sh
+1 -1 metaprl-branches/new_binary_io/util/do-check-all.sh