Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-12-12 16:50:03 -0800 (Mon, 12 Dec 2005)
Revision: 8282
Log message:

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

Changes  Path
+95 -36 metaprl-branches/new_binary_io/OMakefile
+2 -2 metaprl-branches/new_binary_io/doc/htmlman/mp-svn-rw.html
+1 -2 metaprl-branches/new_binary_io/doc/latex/theories/OMakefile
+10 -14 metaprl-branches/new_binary_io/editor/ml/OMakefile
+59 -78 metaprl-branches/new_binary_io/filter/OMakefile
Properties metaprl-branches/new_binary_io/filter/base
+2 -0 metaprl-branches/new_binary_io/filter/base/filter_grammar.ml
+2 -1 metaprl-branches/new_binary_io/filter/base/filter_io.ml
+243 -136 metaprl-branches/new_binary_io/filter/base/filter_reflection.ml
+2 -0 metaprl-branches/new_binary_io/filter/base/filter_reflection.mli
+6 -4 metaprl-branches/new_binary_io/filter/base/filter_util.ml
+1 -0 metaprl-branches/new_binary_io/filter/filter/OMakefile
Copied metaprl-branches/new_binary_io/filter/filter/filter_merge_prla.ml
Properties metaprl-branches/new_binary_io/filter/filter/filter_merge_prla.ml
+3 -3 metaprl-branches/new_binary_io/filter/filter/filter_parse.ml
+37 -33 metaprl-branches/new_binary_io/filter/filter/filter_prog.ml
+7 -6 metaprl-branches/new_binary_io/filter/filter/term_grammar.ml
+3 -3 metaprl-branches/new_binary_io/mk/defaults
+8 -6 metaprl-branches/new_binary_io/mk/make_config
+5 -1 metaprl-branches/new_binary_io/mk/prlcomp
+193 -256 metaprl-branches/new_binary_io/refiner/refiner/refine.ml
+9 -5 metaprl-branches/new_binary_io/refiner/refiner/refiner_debug.ml
+67 -77 metaprl-branches/new_binary_io/refiner/reflib/ascii_io.ml
+2 -1 metaprl-branches/new_binary_io/refiner/reflib/ascii_io_sig.ml
+1 -1 metaprl-branches/new_binary_io/refiner/reflib/dform.ml
+42 -31 metaprl-branches/new_binary_io/refiner/reflib/jall.ml
+10 -4 metaprl-branches/new_binary_io/refiner/reflib/jordering.ml
+27 -10 metaprl-branches/new_binary_io/refiner/reflib/jtunify.ml
+2 -0 metaprl-branches/new_binary_io/refiner/reflib/jtunify.mli
+16 -12 metaprl-branches/new_binary_io/refiner/reflib/term_ty_infer.ml
+22 -8 metaprl-branches/new_binary_io/refiner/refsig/refine_sig.ml
+8 -0 metaprl-branches/new_binary_io/refiner/refsig/term_man_sig.ml
+2 -1 metaprl-branches/new_binary_io/refiner/refsig/term_meta_sig.ml
+192 -148 metaprl-branches/new_binary_io/refiner/rewrite/rewrite_compile_redex.ml
+8 -3 metaprl-branches/new_binary_io/refiner/rewrite/rewrite_debug.ml
+46 -17 metaprl-branches/new_binary_io/refiner/rewrite/rewrite_match_redex.ml
+4 -0 metaprl-branches/new_binary_io/refiner/rewrite/rewrite_types.ml
+1 -1 metaprl-branches/new_binary_io/refiner/term_ds/term_base_ds.ml
+63 -2 metaprl-branches/new_binary_io/refiner/term_ds/term_man_ds.ml
+2 -2 metaprl-branches/new_binary_io/refiner/term_ds/term_subst_ds.ml
+73 -0 metaprl-branches/new_binary_io/refiner/term_gen/term_man_gen.ml
+3 -3 metaprl-branches/new_binary_io/refiner/term_gen/term_meta_gen.ml
+18 -27 metaprl-branches/new_binary_io/support/display/base_dform.ml
+1 -1 metaprl-branches/new_binary_io/support/display/base_dform.mli
+2 -2 metaprl-branches/new_binary_io/support/display/comment.ml
+11 -1 metaprl-branches/new_binary_io/support/display/perv.ml
+10 -0 metaprl-branches/new_binary_io/support/display/perv.mli
+2 -2 metaprl-branches/new_binary_io/support/display/summary.ml
+11 -3 metaprl-branches/new_binary_io/support/tactics/auto_tactic.ml
+1 -1 metaprl-branches/new_binary_io/support/tactics/top_conversionals.mli
+5 -0 metaprl-branches/new_binary_io/tactics/proof/sequent_boot.ml
+1 -0 metaprl-branches/new_binary_io/tactics/proof/tactic_boot_sig.ml
+2 -0 metaprl-branches/new_binary_io/tactics/proof/tacticals_boot.ml
+0 -3 metaprl-branches/new_binary_io/theories/cic/OMakefile
+4 -6 metaprl-branches/new_binary_io/theories/czf/OMakefile
+164 -320 metaprl-branches/new_binary_io/theories/czf/czf_itt_cyclic_group.prla
+3373 -8121 metaprl-branches/new_binary_io/theories/czf/czf_itt_group_power.prla
+0 -3 metaprl-branches/new_binary_io/theories/experimental/compile/OMakefile
+2 -1 metaprl-branches/new_binary_io/theories/experimental/compile/m-paper-hosc.tex
+7 -4 metaprl-branches/new_binary_io/theories/experimental/compile/m_doc_closure.ml
+6 -1 metaprl-branches/new_binary_io/theories/experimental/compile/m_doc_comment.ml
+2 -0 metaprl-branches/new_binary_io/theories/experimental/compile/m_doc_comment.mli
+6 -4 metaprl-branches/new_binary_io/theories/experimental/compile/m_doc_cps.ml
+25 -19 metaprl-branches/new_binary_io/theories/experimental/compile/m_doc_intro.ml
+28 -8 metaprl-branches/new_binary_io/theories/experimental/compile/m_doc_ir.ml
+5 -5 metaprl-branches/new_binary_io/theories/experimental/compile/m_doc_parsing.ml
+30 -6 metaprl-branches/new_binary_io/theories/experimental/compile/m_doc_summary.ml
+76 -22 metaprl-branches/new_binary_io/theories/experimental/compile/m_doc_x86_asm.ml
+22 -13 metaprl-branches/new_binary_io/theories/experimental/compile/m_doc_x86_codegen.ml
+2 -0 metaprl-branches/new_binary_io/theories/experimental/compile/m_doc_x86_opt.ml
+11 -9 metaprl-branches/new_binary_io/theories/experimental/compile/m_doc_x86_regalloc.ml
+1 -1 metaprl-branches/new_binary_io/theories/experimental/compile/m_ir.ml
+0 -12 metaprl-branches/new_binary_io/theories/experimental/mcc/fir/type/OMakefile
+2 -5 metaprl-branches/new_binary_io/theories/experimental/unity/OMakefile
+0 -6 metaprl-branches/new_binary_io/theories/fir/OMakefile
+2 -4 metaprl-branches/new_binary_io/theories/fol/OMakefile
+0 -3 metaprl-branches/new_binary_io/theories/hol/OMakefile
+3 -5 metaprl-branches/new_binary_io/theories/ilc/OMakefile
+3 -20 metaprl-branches/new_binary_io/theories/itt/OMakefile
+1 -7 metaprl-branches/new_binary_io/theories/itt/applications/OMakefile
+2 -4 metaprl-branches/new_binary_io/theories/itt/applications/algebra/OMakefile
+3965 -4859 metaprl-branches/new_binary_io/theories/itt/applications/algebra/itt_cyclic_group.prla
+8611 -8870 metaprl-branches/new_binary_io/theories/itt/applications/algebra/itt_group.prla
+3919 -4226 metaprl-branches/new_binary_io/theories/itt/applications/algebra/itt_poly.prla
+2 -4 metaprl-branches/new_binary_io/theories/itt/applications/datatypes/OMakefile
+2 -2 metaprl-branches/new_binary_io/theories/itt/applications/datatypes/itt_fset.prla
+3 -5 metaprl-branches/new_binary_io/theories/itt/applications/function_spaces/OMakefile
+2 -4 metaprl-branches/new_binary_io/theories/itt/applications/objects/OMakefile
+63 -5 metaprl-branches/new_binary_io/theories/itt/applications/objects/itt_obj_base_rewrite.ml
+971 -827 metaprl-branches/new_binary_io/theories/itt/applications/objects/itt_obj_base_rewrite.prla
+3 -5 metaprl-branches/new_binary_io/theories/itt/applications/supinf/OMakefile
+1 -4 metaprl-branches/new_binary_io/theories/itt/core/OMakefile
+1 -1 metaprl-branches/new_binary_io/theories/itt/core/itt_bool.prla
+1 -1 metaprl-branches/new_binary_io/theories/itt/core/itt_image.prla
+1 -1 metaprl-branches/new_binary_io/theories/itt/core/itt_int_arith.ml
+19042 -19203 metaprl-branches/new_binary_io/theories/itt/core/itt_int_arith.prla
+38 -25 metaprl-branches/new_binary_io/theories/itt/core/itt_int_base.ml
+1 -0 metaprl-branches/new_binary_io/theories/itt/core/itt_int_base.mli
+8337 -7959 metaprl-branches/new_binary_io/theories/itt/core/itt_int_base.prla
+102 -65 metaprl-branches/new_binary_io/theories/itt/core/itt_int_ext.ml
+0 -1 metaprl-branches/new_binary_io/theories/itt/core/itt_int_ext.mli
+12601 -11015 metaprl-branches/new_binary_io/theories/itt/core/itt_int_ext.prla
+10 -5 metaprl-branches/new_binary_io/theories/itt/core/itt_list.ml
+2845 -2781 metaprl-branches/new_binary_io/theories/itt/core/itt_list.prla
+76 -0 metaprl-branches/new_binary_io/theories/itt/core/itt_list2.ml
+2 -0 metaprl-branches/new_binary_io/theories/itt/core/itt_list2.mli
+10661 -9587 metaprl-branches/new_binary_io/theories/itt/core/itt_list2.prla
+9 -9 metaprl-branches/new_binary_io/theories/itt/core/itt_nat.ml
+2647 -4178 metaprl-branches/new_binary_io/theories/itt/core/itt_nat.prla
+12 -2 metaprl-branches/new_binary_io/theories/itt/core/itt_omega.ml
+42049 -42268 metaprl-branches/new_binary_io/theories/itt/core/itt_omega.prla
+3 -3 metaprl-branches/new_binary_io/theories/itt/core/itt_pointwise2.prla
+2 -2 metaprl-branches/new_binary_io/theories/itt/core/itt_quotient.prla
+2 -2 metaprl-branches/new_binary_io/theories/itt/core/itt_record.prla
+3 -3 metaprl-branches/new_binary_io/theories/itt/core/itt_record_exm.prla
+43 -0 metaprl-branches/new_binary_io/theories/itt/core/itt_squiggle.mli
+27 -8 metaprl-branches/new_binary_io/theories/itt/core/itt_struct.ml
+1 -0 metaprl-branches/new_binary_io/theories/itt/core/itt_struct.mli
+1 -1 metaprl-branches/new_binary_io/theories/itt/core/itt_struct2.prla
+1 -1 metaprl-branches/new_binary_io/theories/itt/core/itt_struct3.prla
+4 -26 metaprl-branches/new_binary_io/theories/itt/extensions/OMakefile
Copied metaprl-branches/new_binary_io/theories/itt/extensions/base
Properties metaprl-branches/new_binary_io/theories/itt/extensions/base
Deleted metaprl-branches/new_binary_io/theories/itt/extensions/ctt_markov.ml
Deleted metaprl-branches/new_binary_io/theories/itt/extensions/ctt_markov.mli
Deleted metaprl-branches/new_binary_io/theories/itt/extensions/ctt_markov.prla
Deleted metaprl-branches/new_binary_io/theories/itt/extensions/itt_antiquotient.ml
Deleted metaprl-branches/new_binary_io/theories/itt/extensions/itt_antiquotient.mli
Deleted metaprl-branches/new_binary_io/theories/itt/extensions/itt_antiquotient.prla
Deleted metaprl-branches/new_binary_io/theories/itt/extensions/itt_eta.ml
Deleted metaprl-branches/new_binary_io/theories/itt/extensions/itt_eta.mli
Deleted metaprl-branches/new_binary_io/theories/itt/extensions/itt_eta.prla
Deleted metaprl-branches/new_binary_io/theories/itt/extensions/itt_pairwise.ml
Deleted metaprl-branches/new_binary_io/theories/itt/extensions/itt_pairwise.mli
Deleted metaprl-branches/new_binary_io/theories/itt/extensions/itt_pairwise.prla
Deleted metaprl-branches/new_binary_io/theories/itt/extensions/itt_pairwise2.ml
Deleted metaprl-branches/new_binary_io/theories/itt/extensions/itt_pairwise2.mli
Deleted metaprl-branches/new_binary_io/theories/itt/extensions/itt_pairwise2.prla
Deleted metaprl-branches/new_binary_io/theories/itt/extensions/pairwise-verification.ml
+2 -4 metaprl-branches/new_binary_io/theories/itt/extensions/rfun/OMakefile
Copied metaprl-branches/new_binary_io/theories/itt/extensions/vector
Properties metaprl-branches/new_binary_io/theories/itt/extensions/vector
+1 -7 metaprl-branches/new_binary_io/theories/itt/reflection/OMakefile
+5 -4 metaprl-branches/new_binary_io/theories/itt/reflection/core/OMakefile
+27 -2 metaprl-branches/new_binary_io/theories/itt/reflection/core/itt_hoas_debruijn.ml
+1 -0 metaprl-branches/new_binary_io/theories/itt/reflection/core/itt_hoas_debruijn.mli
+1003 -298 metaprl-branches/new_binary_io/theories/itt/reflection/core/itt_hoas_debruijn.prla
+8 -4 metaprl-branches/new_binary_io/theories/itt/reflection/core/itt_hoas_destterm.mli
+1 -1 metaprl-branches/new_binary_io/theories/itt/reflection/core/itt_hoas_operator.ml
Copied metaprl-branches/new_binary_io/theories/itt/reflection/core/itt_hoas_vbind.ml
Properties metaprl-branches/new_binary_io/theories/itt/reflection/core/itt_hoas_vbind.ml
Copied metaprl-branches/new_binary_io/theories/itt/reflection/core/itt_hoas_vbind.mli
Properties metaprl-branches/new_binary_io/theories/itt/reflection/core/itt_hoas_vbind.mli
Copied metaprl-branches/new_binary_io/theories/itt/reflection/core/itt_hoas_vbind.prla
Properties metaprl-branches/new_binary_io/theories/itt/reflection/core/itt_hoas_vbind.prla
+16 -19 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/OMakefile
+140 -6 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_bterm.ml
+8 -1 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_bterm.mli
+6060 -1899 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_bterm.prla
+22 -1 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_lang.ml
+1755 -1486 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_lang.prla
+1 -1 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_meta_types.ml
+1 -1 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_meta_types.mli
Deleted metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_olang.ml
Deleted metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_olang.mli
Deleted metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_olang.prla
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_proof.ml
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_proof.ml
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_proof.mli
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_proof.mli
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_proof.prla
Properties 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_sequent.ml
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent.ml
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent.mli
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent.mli
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent.prla
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent.prla
Deleted metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_native.ml
Deleted metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_native.mli
Deleted 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_sequent_proof.ml
Properties 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.mli
Properties 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.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_provable.ml
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_provable.ml
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_provable.mli
Properties 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_tactics.ml
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_tactics.ml
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_tactics.mli
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_tactics.mli
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_term1.ml
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_term1.ml
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_term1.mli
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_term1.mli
Copied metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_term1.prla
Properties metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_sequent_term1.prla
+5 -1 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_theory.ml
+4 -1 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_theory.mli
+16 -0 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_util.ml
+12 -0 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/itt_hoas_util.mli
+4 -6 metaprl-branches/new_binary_io/theories/itt/reflection/experimental/jyh/OMakefile
+4 -6 metaprl-branches/new_binary_io/theories/itt/reflection/obsolete/OMakefile
+3 -5 metaprl-branches/new_binary_io/theories/itt/tests/OMakefile
+2 -4 metaprl-branches/new_binary_io/theories/kat/OMakefile
+2 -4 metaprl-branches/new_binary_io/theories/mesa/OMakefile
Copied metaprl-branches/new_binary_io/theories/meta
+0 -3 metaprl-branches/new_binary_io/theories/ocaml_doc/OMakefile
+0 -3 metaprl-branches/new_binary_io/theories/ocaml_sos/OMakefile
+4 -7 metaprl-branches/new_binary_io/theories/poplmark/naive/OMakefile
+1 -1 metaprl-branches/new_binary_io/theories/poplmark/naive/pmn_core_logic.ml
+0 -3 metaprl-branches/new_binary_io/theories/s4lp/OMakefile
+2 -4 metaprl-branches/new_binary_io/theories/sil/OMakefile
+2 -4 metaprl-branches/new_binary_io/theories/tptp/OMakefile
+2 -4 metaprl-branches/new_binary_io/theories/tutorial/OMakefile
+2 -2 metaprl-branches/new_binary_io/util/gen_refiner_debug.pl