Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-07 01:22:48 -0800 (Mon, 07 Nov 2005)
Revision: 8124
Log message:

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

Changes  Path
+2 -2 metaprl-branches/new_binary_io/doc/htmlman/mp-install.html
+1 -0 metaprl-branches/new_binary_io/filter/base/Files
+12 -7 metaprl-branches/new_binary_io/filter/base/OMakefile
+0 -2 metaprl-branches/new_binary_io/filter/base/filter_cache_fun.ml
+1 -412 metaprl-branches/new_binary_io/filter/base/filter_grammar.ml
+1 -8 metaprl-branches/new_binary_io/filter/base/filter_grammar.mli
+3 -2 metaprl-branches/new_binary_io/filter/base/filter_io.ml
Copied metaprl-branches/new_binary_io/filter/base/filter_reflection.ml
Properties metaprl-branches/new_binary_io/filter/base/filter_reflection.ml
Copied metaprl-branches/new_binary_io/filter/base/filter_reflection.mli
Properties metaprl-branches/new_binary_io/filter/base/filter_reflection.mli
+1 -2 metaprl-branches/new_binary_io/filter/base/filter_summary_type.ml
+9 -3 metaprl-branches/new_binary_io/filter/base/filter_type.ml
+7 -1 metaprl-branches/new_binary_io/filter/base/filter_util.ml
+1 -0 metaprl-branches/new_binary_io/filter/base/filter_util.mli
+321 -16 metaprl-branches/new_binary_io/filter/filter/filter_parse.ml
+15 -4 metaprl-branches/new_binary_io/filter/filter/term_grammar.ml
+1 -0 metaprl-branches/new_binary_io/mllib/env_arg.ml
+8 -7 metaprl-branches/new_binary_io/mllib/env_arg.mli
+7 -0 metaprl-branches/new_binary_io/refiner/refiner/refiner_debug.ml
+6 -10 metaprl-branches/new_binary_io/refiner/reflib/jall.ml
+2 -2 metaprl-branches/new_binary_io/refiner/reflib/term_ty_infer.ml
+1 -0 metaprl-branches/new_binary_io/refiner/refsig/term_op_sig.ml
+2 -0 metaprl-branches/new_binary_io/refiner/rewrite/rewrite.ml
+1 -1 metaprl-branches/new_binary_io/refiner/rewrite/rewrite_compile_contractum.ml
+7 -5 metaprl-branches/new_binary_io/refiner/rewrite/rewrite_compile_redex.ml
+2 -0 metaprl-branches/new_binary_io/refiner/rewrite/rewrite_debug.ml
+3 -0 metaprl-branches/new_binary_io/refiner/rewrite/rewrite_types.ml
+28 -2 metaprl-branches/new_binary_io/refiner/rewrite/rewrite_util.ml
+2 -1 metaprl-branches/new_binary_io/refiner/rewrite/rewrite_util_sig.ml
+5 -0 metaprl-branches/new_binary_io/refiner/term_ds/term_op_ds.ml
+5 -0 metaprl-branches/new_binary_io/refiner/term_std/term_op_std.ml
+1 -1 metaprl-branches/new_binary_io/support/display/perv.mli
+4 -0 metaprl-branches/new_binary_io/support/shell/proof_edit.ml
+123 -81 metaprl-branches/new_binary_io/support/tactics/dtactic.ml
+2 -1 metaprl-branches/new_binary_io/support/tactics/dtactic.mli
+23 -1 metaprl-branches/new_binary_io/support/tactics/top_tacticals.ml
+24 -6 metaprl-branches/new_binary_io/support/tactics/top_tacticals.mli
+170 -123 metaprl-branches/new_binary_io/tactics/proof/proof_boot.ml
+19 -0 metaprl-branches/new_binary_io/tactics/proof/proof_term_boot.ml
+2 -0 metaprl-branches/new_binary_io/tactics/proof/sequent_boot.ml
+157 -28 metaprl-branches/new_binary_io/tactics/proof/tactic_boot.ml
+67 -3 metaprl-branches/new_binary_io/tactics/proof/tactic_boot_sig.ml
+51 -19 metaprl-branches/new_binary_io/tactics/proof/tacticals_boot.ml
+11 -0 metaprl-branches/new_binary_io/theories/base/base_grammar.mli
+1 -0 metaprl-branches/new_binary_io/theories/czf/OMakefile
+2125 -2882 metaprl-branches/new_binary_io/theories/czf/czf_itt_abel_group.prla
+1313 -2325 metaprl-branches/new_binary_io/theories/czf/czf_itt_all.prla
+1038 -1842 metaprl-branches/new_binary_io/theories/czf/czf_itt_and.prla
+3808 -5404 metaprl-branches/new_binary_io/theories/czf/czf_itt_cyclic_group.prla
+3083 -4182 metaprl-branches/new_binary_io/theories/czf/czf_itt_cyclic_subgroup.prla
+1861 -2376 metaprl-branches/new_binary_io/theories/czf/czf_itt_empty.prla
+9610 -13455 metaprl-branches/new_binary_io/theories/czf/czf_itt_equiv.prla
+1290 -2199 metaprl-branches/new_binary_io/theories/czf/czf_itt_exists.prla
+757 -1211 metaprl-branches/new_binary_io/theories/czf/czf_itt_false.prla
+4865 -6086 metaprl-branches/new_binary_io/theories/czf/czf_itt_group.prla
+3211 -4490 metaprl-branches/new_binary_io/theories/czf/czf_itt_group_bvd.prla
+1192 -2036 metaprl-branches/new_binary_io/theories/czf/czf_itt_implies.prla
+2567 -3464 metaprl-branches/new_binary_io/theories/czf/czf_itt_inv_image.prla
+3195 -4163 metaprl-branches/new_binary_io/theories/czf/czf_itt_isect.prla
+8163 -9689 metaprl-branches/new_binary_io/theories/czf/czf_itt_kleingroup.prla
+1083 -1830 metaprl-branches/new_binary_io/theories/czf/czf_itt_or.prla
+2739 -3321 metaprl-branches/new_binary_io/theories/czf/czf_itt_rel.prla
+2321 -3047 metaprl-branches/new_binary_io/theories/czf/czf_itt_sall.prla
+5143 -7874 metaprl-branches/new_binary_io/theories/czf/czf_itt_set_ind.prla
+1668 -2663 metaprl-branches/new_binary_io/theories/czf/czf_itt_setdiff.prla
+2398 -3102 metaprl-branches/new_binary_io/theories/czf/czf_itt_sexists.prla
+2565 -3401 metaprl-branches/new_binary_io/theories/czf/czf_itt_singleton.prla
+3830 -5422 metaprl-branches/new_binary_io/theories/czf/czf_itt_subgroup.prla
+2246 -2873 metaprl-branches/new_binary_io/theories/czf/czf_itt_subset.prla
+758 -1211 metaprl-branches/new_binary_io/theories/czf/czf_itt_true.prla
+1678 -2429 metaprl-branches/new_binary_io/theories/fol/cfol_itt_base.prla
+668 -1030 metaprl-branches/new_binary_io/theories/fol/fol_itt_false.prla
+1081 -1504 metaprl-branches/new_binary_io/theories/fol/fol_itt_implies.prla
+646 -992 metaprl-branches/new_binary_io/theories/fol/fol_itt_true.prla
+1 -1 metaprl-branches/new_binary_io/theories/itt/applications/algebra/itt_group.ml
+5703 -6472 metaprl-branches/new_binary_io/theories/itt/applications/algebra/itt_intdomain.prla
+2837 -2701 metaprl-branches/new_binary_io/theories/itt/applications/algebra/itt_intdomain_e.prla
+5012 -6144 metaprl-branches/new_binary_io/theories/itt/applications/datatypes/itt_collection.prla
+1 -1 metaprl-branches/new_binary_io/theories/itt/applications/datatypes/itt_rbtree.ml
+2 -2 metaprl-branches/new_binary_io/theories/itt/core/itt_esquash.ml
+2 -3 metaprl-branches/new_binary_io/theories/itt/core/itt_list.ml
+5862 -5988 metaprl-branches/new_binary_io/theories/itt/core/itt_list.prla
+5 -0 metaprl-branches/new_binary_io/theories/itt/core/itt_list2.ml
+4 -0 metaprl-branches/new_binary_io/theories/itt/core/itt_list2.mli
+844 -866 metaprl-branches/new_binary_io/theories/itt/core/itt_list2.prla
+72 -60 metaprl-branches/new_binary_io/theories/itt/core/itt_logic.ml
+584 -858 metaprl-branches/new_binary_io/theories/itt/core/itt_pointwise.prla
+2 -2 metaprl-branches/new_binary_io/theories/itt/core/itt_quotient.ml
+1932 -2489 metaprl-branches/new_binary_io/theories/itt/core/itt_singleton.prla
+1 -1 metaprl-branches/new_binary_io/theories/itt/core/itt_subtype.ml
+10 -10 metaprl-branches/new_binary_io/theories/itt/core/itt_tunion.ml
+1018 -894 metaprl-branches/new_binary_io/theories/itt/core/itt_tunion.prla
+2129 -3820 metaprl-branches/new_binary_io/theories/itt/core/itt_well_founded.prla
+1038 -825 metaprl-branches/new_binary_io/theories/itt/extensions/itt_pairwise.prla
+75 -103 metaprl-branches/new_binary_io/theories/itt/extensions/pairwise-verification.ml
+1 -1 metaprl-branches/new_binary_io/theories/itt/reflection/core/itt_hoas_base.ml
+4 -4 metaprl-branches/new_binary_io/theories/itt/reflection/core/itt_hoas_vector.ml
+2 -2 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/OMakefile
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_meta_types.ml
Properties 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_meta_types.mli
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_meta_types.mli
+142 -70 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_native.ml
+15 -3 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_native.mli
+1922 -2567 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_native.prla
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_theory.ml
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_theory.ml
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_theory.mli
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_theory.mli
+2 -2 metaprl-branches/new_binary_io/theories/poplmark/naive/OMakefile
Deleted metaprl-branches/new_binary_io/theories/poplmark/naive/pmn_core_judgments.ml
Deleted metaprl-branches/new_binary_io/theories/poplmark/naive/pmn_core_judgments.mli
Copied metaprl-branches/new_binary_io/theories/poplmark/naive/pmn_core_logic.ml
Properties metaprl-branches/new_binary_io/theories/poplmark/naive/pmn_core_logic.ml
Copied metaprl-branches/new_binary_io/theories/poplmark/naive/pmn_core_logic.mli
Properties metaprl-branches/new_binary_io/theories/poplmark/naive/pmn_core_logic.mli
Deleted metaprl-branches/new_binary_io/theories/poplmark/naive/pmn_core_subtype.ml
Deleted metaprl-branches/new_binary_io/theories/poplmark/naive/pmn_core_subtype.mli
+69 -221 metaprl-branches/new_binary_io/theories/poplmark/naive/pmn_core_terms.ml
+65 -50 metaprl-branches/new_binary_io/theories/poplmark/naive/pmn_core_terms.mli
+2426 -3357 metaprl-branches/new_binary_io/theories/poplmark/naive/pmn_core_terms.prla
Deleted metaprl-branches/new_binary_io/theories/poplmark/naive/pmn_core_terms_old.ml
Deleted metaprl-branches/new_binary_io/theories/poplmark/naive/pmn_core_terms_old.mli
Deleted metaprl-branches/new_binary_io/theories/poplmark/naive/pmn_core_terms_old.prla
Copied metaprl-branches/new_binary_io/theories/poplmark/naive/pmn_core_terms_test.ml
Properties metaprl-branches/new_binary_io/theories/poplmark/naive/pmn_core_terms_test.ml
Copied metaprl-branches/new_binary_io/theories/poplmark/naive/pmn_core_terms_test.mli
Properties metaprl-branches/new_binary_io/theories/poplmark/naive/pmn_core_terms_test.mli
Copied metaprl-branches/new_binary_io/theories/poplmark/naive/pmn_core_terms_test.prla
Properties metaprl-branches/new_binary_io/theories/poplmark/naive/pmn_core_terms_test.prla
+7145 -6474 metaprl-branches/new_binary_io/theories/s4lp/s4_logic.prla
+2862 -3197 metaprl-branches/new_binary_io/theories/tptp/tptp_derive.prla