Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-10-12 18:14:08 -0700 (Mon, 12 Oct 1998)
Revision: 2494
Log message:

      I changed all the obvious places of Nuprl-Light, NL, nl, or any
      other instance to MetaPRL, MP, or mp, etc.  The docs may be broken
      but I'll fix them soon.  As usual, let me know if anything breaks.
      

Changes	Path
Deleted	metaprl/.cpdir
Deleted	metaprl/.cprc
+1 -0	metaprl/Makefile
+3 -3	metaprl/doc/htmlman/default.html
+3 -3	metaprl/doc/htmlman/framework/default.html
Added	metaprl/doc/htmlman/framework/mp-framework.html
Properties	metaprl/doc/htmlman/framework/mp-framework.html
Added	metaprl/doc/htmlman/framework/mp-index.html
Properties	metaprl/doc/htmlman/framework/mp-index.html
Deleted	metaprl/doc/htmlman/framework/nl-framework.html
Deleted	metaprl/doc/htmlman/framework/nl-index.html
Binary	metaprl/doc/htmlman/images/mp-logo.gif
Properties	metaprl/doc/htmlman/images/mp-logo.gif
Binary	metaprl/doc/htmlman/images/nl-logo.gif
+2 -2	metaprl/doc/htmlman/license.html
Added	metaprl/doc/htmlman/mp-frame.html
Properties	metaprl/doc/htmlman/mp-frame.html
Added	metaprl/doc/htmlman/mp-index.html
Properties	metaprl/doc/htmlman/mp-index.html
Added	metaprl/doc/htmlman/mp-install.html
Properties	metaprl/doc/htmlman/mp-install.html
Added	metaprl/doc/htmlman/mp-links.html
Properties	metaprl/doc/htmlman/mp-links.html
Added	metaprl/doc/htmlman/mp-people.html
Properties	metaprl/doc/htmlman/mp-people.html
Added	metaprl/doc/htmlman/mp.html
Properties	metaprl/doc/htmlman/mp.html
Deleted	metaprl/doc/htmlman/nl-frame.html
Deleted	metaprl/doc/htmlman/nl-index.html
Deleted	metaprl/doc/htmlman/nl-install.html
Deleted	metaprl/doc/htmlman/nl-links.html
Deleted	metaprl/doc/htmlman/nl-people.html
Deleted	metaprl/doc/htmlman/nl.html
+3 -3	metaprl/doc/htmlman/system/default.html
Added	metaprl/doc/htmlman/system/mp-arch.ai
Properties	metaprl/doc/htmlman/system/mp-arch.ai
Added	metaprl/doc/htmlman/system/mp-arch.gif
Properties	metaprl/doc/htmlman/system/mp-arch.gif
Added	metaprl/doc/htmlman/system/mp-arch.html
Properties	metaprl/doc/htmlman/system/mp-arch.html
Added	metaprl/doc/htmlman/system/mp-arch.map
Properties	metaprl/doc/htmlman/system/mp-arch.map
Added	metaprl/doc/htmlman/system/mp-auto-tactic.html
Properties	metaprl/doc/htmlman/system/mp-auto-tactic.html
Added	metaprl/doc/htmlman/system/mp-base-cache.html
Properties	metaprl/doc/htmlman/system/mp-base-cache.html
Added	metaprl/doc/htmlman/system/mp-base-syntax.html
Properties	metaprl/doc/htmlman/system/mp-base-syntax.html
Added	metaprl/doc/htmlman/system/mp-base.html
Properties	metaprl/doc/htmlman/system/mp-base.html
Added	metaprl/doc/htmlman/system/mp-chaining.html
Properties	metaprl/doc/htmlman/system/mp-chaining.html
Added	metaprl/doc/htmlman/system/mp-conversionals.html
Properties	metaprl/doc/htmlman/system/mp-conversionals.html
Added	metaprl/doc/htmlman/system/mp-dist-tactic.html
Properties	metaprl/doc/htmlman/system/mp-dist-tactic.html
Added	metaprl/doc/htmlman/system/mp-editor-imp.html
Properties	metaprl/doc/htmlman/system/mp-editor-imp.html
Added	metaprl/doc/htmlman/system/mp-ensemble.html
Properties	metaprl/doc/htmlman/system/mp-ensemble.html
Added	metaprl/doc/htmlman/system/mp-filter.html
Properties	metaprl/doc/htmlman/system/mp-filter.html
Added	metaprl/doc/htmlman/system/mp-index.html
Properties	metaprl/doc/htmlman/system/mp-index.html
Added	metaprl/doc/htmlman/system/mp-itt.html
Properties	metaprl/doc/htmlman/system/mp-itt.html
Added	metaprl/doc/htmlman/system/mp-ocaml.html
Properties	metaprl/doc/htmlman/system/mp-ocaml.html
Added	metaprl/doc/htmlman/system/mp-refine.html
Properties	metaprl/doc/htmlman/system/mp-refine.html
Added	metaprl/doc/htmlman/system/mp-refiner.html
Properties	metaprl/doc/htmlman/system/mp-refiner.html
Added	metaprl/doc/htmlman/system/mp-rewrite.html
Properties	metaprl/doc/htmlman/system/mp-rewrite.html
Added	metaprl/doc/htmlman/system/mp-system.html
Properties	metaprl/doc/htmlman/system/mp-system.html
Added	metaprl/doc/htmlman/system/mp-tactic.html
Properties	metaprl/doc/htmlman/system/mp-tactic.html
Added	metaprl/doc/htmlman/system/mp-tacticals.html
Properties	metaprl/doc/htmlman/system/mp-tacticals.html
Added	metaprl/doc/htmlman/system/mp-terms.html
Properties	metaprl/doc/htmlman/system/mp-terms.html
Added	metaprl/doc/htmlman/system/mp-type-inf-rsrc.html
Properties	metaprl/doc/htmlman/system/mp-type-inf-rsrc.html
Binary	metaprl/doc/htmlman/system/nl-arch.ai
Binary	metaprl/doc/htmlman/system/nl-arch.gif
Deleted	metaprl/doc/htmlman/system/nl-arch.html
Deleted	metaprl/doc/htmlman/system/nl-arch.map
Deleted	metaprl/doc/htmlman/system/nl-auto-tactic.html
Deleted	metaprl/doc/htmlman/system/nl-base-cache.html
Deleted	metaprl/doc/htmlman/system/nl-base-syntax.html
Deleted	metaprl/doc/htmlman/system/nl-base.html
Deleted	metaprl/doc/htmlman/system/nl-chaining.html
Deleted	metaprl/doc/htmlman/system/nl-conversionals.html
Deleted	metaprl/doc/htmlman/system/nl-dist-tactic.html
Deleted	metaprl/doc/htmlman/system/nl-editor-imp.html
Deleted	metaprl/doc/htmlman/system/nl-ensemble.html
Deleted	metaprl/doc/htmlman/system/nl-filter.html
Deleted	metaprl/doc/htmlman/system/nl-index.html
Deleted	metaprl/doc/htmlman/system/nl-itt.html
Deleted	metaprl/doc/htmlman/system/nl-ocaml.html
Deleted	metaprl/doc/htmlman/system/nl-refine.html
Deleted	metaprl/doc/htmlman/system/nl-refiner.html
Deleted	metaprl/doc/htmlman/system/nl-rewrite.html
Deleted	metaprl/doc/htmlman/system/nl-system.html
Deleted	metaprl/doc/htmlman/system/nl-tactic.html
Deleted	metaprl/doc/htmlman/system/nl-tacticals.html
Deleted	metaprl/doc/htmlman/system/nl-terms.html
Deleted	metaprl/doc/htmlman/system/nl-type-inf-rsrc.html
Deleted	metaprl/doc/htmlman/system/nl_d_tactic.html
+3 -3	metaprl/doc/htmlman/tutorial/default.html
Added	metaprl/doc/htmlman/tutorial/mp-all.html
Properties	metaprl/doc/htmlman/tutorial/mp-all.html
Added	metaprl/doc/htmlman/tutorial/mp-base-auto.html
Properties	metaprl/doc/htmlman/tutorial/mp-base-auto.html
Added	metaprl/doc/htmlman/tutorial/mp-base.html
Properties	metaprl/doc/htmlman/tutorial/mp-base.html
Added	metaprl/doc/htmlman/tutorial/mp-class.html
Properties	metaprl/doc/htmlman/tutorial/mp-class.html
Added	metaprl/doc/htmlman/tutorial/mp-ctheory.html
Properties	metaprl/doc/htmlman/tutorial/mp-ctheory.html
Added	metaprl/doc/htmlman/tutorial/mp-getting-started.html
Properties	metaprl/doc/htmlman/tutorial/mp-getting-started.html
Added	metaprl/doc/htmlman/tutorial/mp-index.html
Properties	metaprl/doc/htmlman/tutorial/mp-index.html
Added	metaprl/doc/htmlman/tutorial/mp-not.html
Properties	metaprl/doc/htmlman/tutorial/mp-not.html
Added	metaprl/doc/htmlman/tutorial/mp-simple.html
Properties	metaprl/doc/htmlman/tutorial/mp-simple.html
Added	metaprl/doc/htmlman/tutorial/mp-struct.html
Properties	metaprl/doc/htmlman/tutorial/mp-struct.html
Added	metaprl/doc/htmlman/tutorial/mp-theory.html
Properties	metaprl/doc/htmlman/tutorial/mp-theory.html
Added	metaprl/doc/htmlman/tutorial/mp-tutorial.html
Properties	metaprl/doc/htmlman/tutorial/mp-tutorial.html
Added	metaprl/doc/htmlman/tutorial/mp-type.html
Properties	metaprl/doc/htmlman/tutorial/mp-type.html
Deleted	metaprl/doc/htmlman/tutorial/nl-all.html
Deleted	metaprl/doc/htmlman/tutorial/nl-base-auto.html
Deleted	metaprl/doc/htmlman/tutorial/nl-base.html
Deleted	metaprl/doc/htmlman/tutorial/nl-class.html
Deleted	metaprl/doc/htmlman/tutorial/nl-ctheory.html
Deleted	metaprl/doc/htmlman/tutorial/nl-getting-started.html
Deleted	metaprl/doc/htmlman/tutorial/nl-index.html
Deleted	metaprl/doc/htmlman/tutorial/nl-not.html
Deleted	metaprl/doc/htmlman/tutorial/nl-simple.html
Deleted	metaprl/doc/htmlman/tutorial/nl-struct.html
Deleted	metaprl/doc/htmlman/tutorial/nl-theory.html
Deleted	metaprl/doc/htmlman/tutorial/nl-tutorial.html
Deleted	metaprl/doc/htmlman/tutorial/nl-type.html
+3 -3	metaprl/doc/htmlman/user-guide/default.html
Added	metaprl/doc/htmlman/user-guide/mp-axiom.html
Properties	metaprl/doc/htmlman/user-guide/mp-axiom.html
Added	metaprl/doc/htmlman/user-guide/mp-dform.html
Properties	metaprl/doc/htmlman/user-guide/mp-dform.html
Added	metaprl/doc/htmlman/user-guide/mp-editor.html
Properties	metaprl/doc/htmlman/user-guide/mp-editor.html
Added	metaprl/doc/htmlman/user-guide/mp-index.html
Properties	metaprl/doc/htmlman/user-guide/mp-index.html
Added	metaprl/doc/htmlman/user-guide/mp-modules.html
Properties	metaprl/doc/htmlman/user-guide/mp-modules.html
Added	metaprl/doc/htmlman/user-guide/mp-rewrite.html
Properties	metaprl/doc/htmlman/user-guide/mp-rewrite.html
Added	metaprl/doc/htmlman/user-guide/mp-terms.html
Properties	metaprl/doc/htmlman/user-guide/mp-terms.html
Added	metaprl/doc/htmlman/user-guide/mp-user-guide.html
Properties	metaprl/doc/htmlman/user-guide/mp-user-guide.html
Deleted	metaprl/doc/htmlman/user-guide/nl-axiom.html
Deleted	metaprl/doc/htmlman/user-guide/nl-dform.html
Deleted	metaprl/doc/htmlman/user-guide/nl-editor.html
Deleted	metaprl/doc/htmlman/user-guide/nl-index.html
Deleted	metaprl/doc/htmlman/user-guide/nl-modules.html
Deleted	metaprl/doc/htmlman/user-guide/nl-rewrite.html
Deleted	metaprl/doc/htmlman/user-guide/nl-terms.html
Deleted	metaprl/doc/htmlman/user-guide/nl-user-guide.html
Properties	metaprl/editor/ml
+19 -19	metaprl/editor/ml/Makefile
+3 -3	metaprl/editor/ml/czf.ml
+5 -5	metaprl/editor/ml/io_proof.ml
+1 -1	metaprl/editor/ml/io_proof.mli
+1 -1	metaprl/editor/ml/io_proof_type.mlz
+38 -38	metaprl/editor/ml/library_eval.ml
+1 -1	metaprl/editor/ml/library_eval.mli
+2 -2	metaprl/editor/ml/library_test.ml
+1 -1	metaprl/editor/ml/library_test.mli
Added	metaprl/editor/ml/mp
Properties	metaprl/editor/ml/mp
Added	metaprl/editor/ml/mp.ml
Properties	metaprl/editor/ml/mp.ml
Added	metaprl/editor/ml/mp.mli
Properties	metaprl/editor/ml/mp.mli
Added	metaprl/editor/ml/mp_top.ml
Properties	metaprl/editor/ml/mp_top.ml
Added	metaprl/editor/ml/mp_top.mli
Properties	metaprl/editor/ml/mp_top.mli
Added	metaprl/editor/ml/mp_version.mli
Properties	metaprl/editor/ml/mp_version.mli
Added	metaprl/editor/ml/mpconfig
Properties	metaprl/editor/ml/mpconfig
Added	metaprl/editor/ml/mpgossip
Properties	metaprl/editor/ml/mpgossip
Added	metaprl/editor/ml/mpopt
Properties	metaprl/editor/ml/mpopt
Added	metaprl/editor/ml/mptop
Properties	metaprl/editor/ml/mptop
Deleted	metaprl/editor/ml/nl
Deleted	metaprl/editor/ml/nl.ml
Deleted	metaprl/editor/ml/nl.mli
Deleted	metaprl/editor/ml/nl_top.ml
Deleted	metaprl/editor/ml/nl_top.mli
Deleted	metaprl/editor/ml/nl_version.mli
Deleted	metaprl/editor/ml/nlconfig
Deleted	metaprl/editor/ml/nlgossip
Deleted	metaprl/editor/ml/nlopt
Deleted	metaprl/editor/ml/nltop
+2 -2	metaprl/editor/ml/package_df.ml
+1 -1	metaprl/editor/ml/package_df.mli
+3 -3	metaprl/editor/ml/package_info.ml
+1 -1	metaprl/editor/ml/package_info.mli
+2 -2	metaprl/editor/ml/package_int.ml
+1 -1	metaprl/editor/ml/package_int.mli
+1 -1	metaprl/editor/ml/package_type.mlz
+2 -2	metaprl/editor/ml/proof.ml
+1 -1	metaprl/editor/ml/proof.mli
+2 -2	metaprl/editor/ml/proof_edit.ml
+1 -1	metaprl/editor/ml/proof_edit.mli
+2 -2	metaprl/editor/ml/proof_step.ml
+1 -1	metaprl/editor/ml/proof_step.mli
+1 -1	metaprl/editor/ml/proof_type.mlz
+4 -4	metaprl/editor/ml/shell.ml
+1 -1	metaprl/editor/ml/shell.mli
Added	metaprl/editor/ml/shell_mp.ml
Properties	metaprl/editor/ml/shell_mp.ml
Added	metaprl/editor/ml/shell_mp.mli
Properties	metaprl/editor/ml/shell_mp.mli
Deleted	metaprl/editor/ml/shell_nl.ml
Deleted	metaprl/editor/ml/shell_nl.mli
+2 -2	metaprl/editor/ml/shell_null.ml
+1 -1	metaprl/editor/ml/shell_null.mli
+7 -7	metaprl/editor/ml/shell_p4.ml
+1 -1	metaprl/editor/ml/shell_p4.mli
+2 -2	metaprl/editor/ml/shell_p4_type.mlz
+2 -2	metaprl/editor/ml/shell_rewrite.ml
+1 -1	metaprl/editor/ml/shell_rewrite.mli
+2 -2	metaprl/editor/ml/shell_rule.ml
+1 -1	metaprl/editor/ml/shell_rule.mli
+1 -1	metaprl/editor/ml/shell_type.mlz
+2 -2	metaprl/editor/ml/test.ml
+1 -1	metaprl/editor/ml/test.mli
+1 -1	metaprl/editor/ml/w.ml
+3 -3	metaprl/editor/ml/x.ml
+3 -3	metaprl/editor/ml/y.ml
+1 -1	metaprl/editor/ml/z.ml
+2 -2	metaprl/ensemble/appl_closure.ml
+1 -1	metaprl/ensemble/appl_closure.mli
+179 -179	metaprl/ensemble/ensemble_queue.ml
+1 -1	metaprl/ensemble/ensemble_queue.mli
+2 -2	metaprl/ensemble/remote_ensemble.ml
+1 -1	metaprl/ensemble/remote_ensemble.mli
+1 -1	metaprl/ensemble/remote_null.ml
+1 -1	metaprl/ensemble/remote_null.mli
+1 -1	metaprl/ensemble/remote_sig.mlz
+1 -1	metaprl/ensemble/thread_refiner.mli
+2 -2	metaprl/ensemble/thread_refiner_ens.ml
+1 -1	metaprl/ensemble/thread_refiner_ens.mli
+1 -1	metaprl/ensemble/thread_refiner_ens_mod.ml
+1 -1	metaprl/ensemble/thread_refiner_null.ml
+1 -1	metaprl/ensemble/thread_refiner_null.mli
+1 -1	metaprl/ensemble/thread_refiner_null_mod.ml
+1 -1	metaprl/ensemble/thread_refiner_sig.mlz
+2 -2	metaprl/evaluator/evaluator.ml
+1 -1	metaprl/evaluator/evaluator.mli
+2 -2	metaprl/evaluator/itt_redrules.ml
+1 -1	metaprl/evaluator/itt_redrules.mli
+3 -3	metaprl/filter/filter_ast.ml
+1 -1	metaprl/filter/filter_ast.mli
+3 -3	metaprl/filter/filter_bin.ml
+1 -1	metaprl/filter/filter_bin.mli
+2 -2	metaprl/filter/filter_buffer.ml
+1 -1	metaprl/filter/filter_buffer.mli
+2 -2	metaprl/filter/filter_cache.ml
+1 -1	metaprl/filter/filter_cache.mli
+3 -3	metaprl/filter/filter_cache_fun.ml
+1 -1	metaprl/filter/filter_cache_fun.mli
+3 -3	metaprl/filter/filter_comment.ml
+1 -1	metaprl/filter/filter_comment.mli
+1 -1	metaprl/filter/filter_debug.ml
+1 -1	metaprl/filter/filter_debug.mli
+2 -2	metaprl/filter/filter_exn.ml
+1 -1	metaprl/filter/filter_exn.mli
+2 -2	metaprl/filter/filter_grammar.ml
+1 -1	metaprl/filter/filter_grammar.mli
+2 -2	metaprl/filter/filter_hash.ml
+1 -1	metaprl/filter/filter_hash.mli
+2 -2	metaprl/filter/filter_html.ml
+1 -1	metaprl/filter/filter_html.mli
+1 -1	metaprl/filter/filter_magic.ml
+1 -1	metaprl/filter/filter_magic.mli
+3 -3	metaprl/filter/filter_main.ml
+1 -1	metaprl/filter/filter_main.mli
+12 -12	metaprl/filter/filter_ocaml.ml
+2 -2	metaprl/filter/filter_ocaml.mli
+4 -4	metaprl/filter/filter_parse.ml
+1 -1	metaprl/filter/filter_parse.mli
+16 -16	metaprl/filter/filter_prog.ml
+1 -1	metaprl/filter/filter_prog.mli
+7 -7	metaprl/filter/filter_summary.ml
+1 -1	metaprl/filter/filter_summary.mli
+2 -2	metaprl/filter/filter_summary_io.ml
+1 -1	metaprl/filter/filter_summary_io.mli
+1 -1	metaprl/filter/filter_summary_param.mlz
+1 -1	metaprl/filter/filter_summary_type.mlz
+3 -3	metaprl/filter/filter_summary_util.ml
+1 -1	metaprl/filter/filter_summary_util.mli
+1 -1	metaprl/filter/filter_type.mlz
+2 -2	metaprl/filter/filter_util.ml
+1 -1	metaprl/filter/filter_util.mli
+2 -2	metaprl/filter/free_vars.ml
+1 -1	metaprl/filter/free_vars.mli
+1 -1	metaprl/filter/infix.mli
+1 -1	metaprl/filter/infix.pre.ml
+2 -2	metaprl/filter/mLast_util.ml
+1 -1	metaprl/filter/mLast_util.mli
+3 -3	metaprl/filter/prlcomp.ml
+2 -2	metaprl/filter/prlcomp.mli
+7 -7	metaprl/filter/term_grammar.ml
+1 -1	metaprl/filter/term_grammar.mli
+2 -2	metaprl/filter/term_quote.ml
+1 -1	metaprl/filter/term_quote.mli
+1 -1	metaprl/filter/test.ml
+1 -1	metaprl/filter/test.mli
+1 -1	metaprl/filter/test_filter.ml
+1 -1	metaprl/filter/test_filter.mli
+1 -1	metaprl/filter/test_gram.ml
+1 -1	metaprl/horus/opname.ml
+1 -1	metaprl/horus/opname.mli
+1 -1	metaprl/horus/term.ml
+2 -2	metaprl/horus/term.mli
+1 -1	metaprl/horus/util.ml
+1 -1	metaprl/horus/util.mli
+3 -3	metaprl/library/ascii_scan.ml
+2 -2	metaprl/library/ascii_scan.mli
+12 -12	metaprl/library/basic.ml
+2 -2	metaprl/library/basic.mli
+2 -2	metaprl/library/bigInt.ml
+1 -1	metaprl/library/bigInt.mli
+13 -13	metaprl/library/db.ml
+1 -1	metaprl/library/db.mli
+2 -2	metaprl/library/definition.ml
+1 -1	metaprl/library/definition.mli
+2 -2	metaprl/library/int32.ml
+1 -1	metaprl/library/int32.mli
+3 -3	metaprl/library/library.ml
+1 -1	metaprl/library/library.mli
+2 -2	metaprl/library/library_type_base.ml
+1 -1	metaprl/library/library_type_base.mli
+3 -3	metaprl/library/link.ml
+1 -1	metaprl/library/link.mli
+9 -9	metaprl/library/mathBus.ml
+2 -2	metaprl/library/mathBus.mli
+4 -4	metaprl/library/mbterm.ml
+1 -1	metaprl/library/mbterm.mli
+6 -6	metaprl/library/nuprl5.ml
+2 -2	metaprl/library/nuprl5.mli
+2 -2	metaprl/library/object_id.ml
+1 -1	metaprl/library/object_id.mli
+2 -2	metaprl/library/oidtable.ml
+1 -1	metaprl/library/oidtable.mli
+5 -5	metaprl/library/orb.ml
+1 -1	metaprl/library/orb.mli
+3 -3	metaprl/library/registry.ml
+1 -1	metaprl/library/registry.mli
+2 -2	metaprl/library/socketIo.ml
+1 -1	metaprl/library/socketIo.mli
+2 -2	metaprl/library/tentfunctor.ml
+1 -1	metaprl/library/tentfunctor.mli
+2 -2	metaprl/library/test.ml
+2 -2	metaprl/library/utils.ml
+1 -1	metaprl/library/utils.mli
Properties	metaprl/mllib
+5 -5	metaprl/mllib/Makefile
+1 -1	metaprl/mllib/array_util.ml
+1 -1	metaprl/mllib/bitset.ml
+1 -1	metaprl/mllib/ctype.ml
+1 -1	metaprl/mllib/cycle_dag.ml
+1 -1	metaprl/mllib/cycle_dag.mli
+1 -1	metaprl/mllib/dag.mlz
+1 -1	metaprl/mllib/debug_set.ml
+2 -2	metaprl/mllib/debug_string_sets.ml
+4 -4	metaprl/mllib/debug_string_sets.mli
+1 -1	metaprl/mllib/env_arg.ml
+1 -1	metaprl/mllib/env_arg.mli
+2 -2	metaprl/mllib/file_base.ml
+1 -1	metaprl/mllib/file_base.mli
+1 -1	metaprl/mllib/file_base_type.ml
+3 -3	metaprl/mllib/file_type_base.ml
+1 -1	metaprl/mllib/file_type_base.mli
+3 -3	metaprl/mllib/file_util.ml
+1 -1	metaprl/mllib/file_util.mli
+2 -2	metaprl/mllib/filename_util.ml
+1 -1	metaprl/mllib/filename_util.mli
+1 -1	metaprl/mllib/flist.ml
+1 -1	metaprl/mllib/flist.mli
+1 -1	metaprl/mllib/fun_splay_set.ml
+2 -2	metaprl/mllib/fun_splay_set.mli
+1 -1	metaprl/mllib/getrusage.ml
+1 -1	metaprl/mllib/getrusage.mli
+1 -1	metaprl/mllib/hash_set.ml
+2 -2	metaprl/mllib/hash_set.mli
+2 -2	metaprl/mllib/imp_dag.ml
+1 -1	metaprl/mllib/imp_dag.mli
+2 -2	metaprl/mllib/list_util.ml
+1 -1	metaprl/mllib/list_util.mli
+2 -2	metaprl/mllib/memo.ml
+1 -1	metaprl/mllib/memo.mli
Added	metaprl/mllib/mp_big_int.ml
Properties	metaprl/mllib/mp_big_int.ml
Added	metaprl/mllib/mp_big_int.mli
Properties	metaprl/mllib/mp_big_int.mli
Added	metaprl/mllib/mp_debug.ml
Properties	metaprl/mllib/mp_debug.ml
Added	metaprl/mllib/mp_debug.mli
Properties	metaprl/mllib/mp_debug.mli
Added	metaprl/mllib/mp_num.ml
Properties	metaprl/mllib/mp_num.ml
Added	metaprl/mllib/mp_num.mli
Properties	metaprl/mllib/mp_num.mli
Added	metaprl/mllib/mp_pervasives.ml
Properties	metaprl/mllib/mp_pervasives.ml
Added	metaprl/mllib/mp_pervasives.mli
Properties	metaprl/mllib/mp_pervasives.mli
Added	metaprl/mllib/mp_set.mlz
Properties	metaprl/mllib/mp_set.mlz
Deleted	metaprl/mllib/nl_big_int.ml
Deleted	metaprl/mllib/nl_big_int.mli
Deleted	metaprl/mllib/nl_debug.ml
Deleted	metaprl/mllib/nl_debug.mli
Deleted	metaprl/mllib/nl_num.ml
Deleted	metaprl/mllib/nl_num.mli
Deleted	metaprl/mllib/nl_pervasives.ml
Deleted	metaprl/mllib/nl_pervasives.mli
Deleted	metaprl/mllib/nl_set.mlz
+2 -2	metaprl/mllib/precedence.ml
+1 -1	metaprl/mllib/precedence.mli
+1 -1	metaprl/mllib/punix.ml
+1 -1	metaprl/mllib/punix.mli
+1 -1	metaprl/mllib/red_black_set.ml
+2 -2	metaprl/mllib/red_black_set.mli
+1 -1	metaprl/mllib/red_black_test.ml
+1 -1	metaprl/mllib/red_black_test.mli
+2 -2	metaprl/mllib/ref_util.ml
+1 -1	metaprl/mllib/ref_util.mli
+1 -1	metaprl/mllib/remote_lazy_queue.ml
+1 -1	metaprl/mllib/remote_lazy_queue.mli
+1 -1	metaprl/mllib/remote_lazy_queue_sig.ml
+2 -2	metaprl/mllib/remote_queue_null.ml
+1 -1	metaprl/mllib/remote_queue_null.mli
+1 -1	metaprl/mllib/remote_queue_sig.ml
+2 -2	metaprl/mllib/small_set.ml
+3 -3	metaprl/mllib/small_set.mli
+1 -1	metaprl/mllib/splay_table.ml
+1 -1	metaprl/mllib/splay_table.mli
+1 -1	metaprl/mllib/string_set.ml
+2 -2	metaprl/mllib/string_set.mli
+2 -2	metaprl/mllib/string_util.ml
+1 -1	metaprl/mllib/string_util.mli
+2 -2	metaprl/mllib/thread_event.ml
+1 -1	metaprl/mllib/thread_event.mli
+1 -1	metaprl/mllib/thread_util.ml
+1 -1	metaprl/mllib/thread_util.mli
+1 -1	metaprl/mllib/unix_util.ml
+1 -1	metaprl/mllib/unix_util.mli
+3 -3	metaprl/refiner/refbase/opname.ml
+1 -1	metaprl/refiner/refbase/opname.mli
+1 -1	metaprl/refiner/refiner/refine.mlip
+2 -2	metaprl/refiner/refiner/refine.mlp
+1 -1	metaprl/refiner/refiner/refine_error.ml
+1 -1	metaprl/refiner/refiner/refine_error.mli
+1 -1	metaprl/refiner/refiner/refiner.ml
+1 -1	metaprl/refiner/refiner/refiner.mli
+1 -1	metaprl/refiner/refiner/refiner_ds_simp.ml
+1 -1	metaprl/refiner/refiner/refiner_ds_simp.mli
+1 -1	metaprl/refiner/refiner/refiner_ds_verb.ml
+1 -1	metaprl/refiner/refiner/refiner_ds_verb.mli
+1 -1	metaprl/refiner/refiner/refiner_std_simp.ml
+1 -1	metaprl/refiner/refiner/refiner_std_simp.mli
+1 -1	metaprl/refiner/refiner/refiner_std_verb.ml
+1 -1	metaprl/refiner/refiner/refiner_std_verb.mli
Properties	metaprl/refiner/reflib
+1 -1	metaprl/refiner/reflib/Files
+2 -2	metaprl/refiner/reflib/dform.ml
+1 -1	metaprl/refiner/reflib/dform.mli
+2 -2	metaprl/refiner/reflib/dform_print.ml
+1 -1	metaprl/refiner/reflib/dform_print.mli
+2 -2	metaprl/refiner/reflib/ml_file.ml
+1 -1	metaprl/refiner/reflib/ml_file.mli
+2 -2	metaprl/refiner/reflib/ml_format.ml
+1 -1	metaprl/refiner/reflib/ml_format.mli
+2 -2	metaprl/refiner/reflib/ml_format_sig.mlz
+3 -3	metaprl/refiner/reflib/ml_print.ml
+1 -1	metaprl/refiner/reflib/ml_print.mli
+1 -1	metaprl/refiner/reflib/ml_print_sig.mlz
+2 -2	metaprl/refiner/reflib/ml_string.ml
+1 -1	metaprl/refiner/reflib/ml_string.mli
+1 -1	metaprl/refiner/reflib/ml_term.ml
+1 -1	metaprl/refiner/reflib/ml_term.mli
Added	metaprl/refiner/reflib/mp_resource.ml
Properties	metaprl/refiner/reflib/mp_resource.ml
Added	metaprl/refiner/reflib/mp_resource.mli
Properties	metaprl/refiner/reflib/mp_resource.mli
Deleted	metaprl/refiner/reflib/nl_resource.ml
Deleted	metaprl/refiner/reflib/nl_resource.mli
+2 -2	metaprl/refiner/reflib/refine_exn.ml
+1 -1	metaprl/refiner/reflib/refine_exn.mli
+3 -3	metaprl/refiner/reflib/rformat.ml
+2 -2	metaprl/refiner/reflib/rformat.mli
+2 -2	metaprl/refiner/reflib/simple_print.ml
+1 -1	metaprl/refiner/reflib/simple_print.mli
+1 -1	metaprl/refiner/reflib/simple_print_sig.ml
+3 -3	metaprl/refiner/reflib/term_copy.ml
+1 -1	metaprl/refiner/reflib/term_copy.mli
+2 -2	metaprl/refiner/reflib/term_dtable.ml
+1 -1	metaprl/refiner/reflib/term_dtable.mli
+2 -2	metaprl/refiner/reflib/term_stable.ml
+1 -1	metaprl/refiner/reflib/term_stable.mli
+2 -2	metaprl/refiner/reflib/term_table.ml
+1 -1	metaprl/refiner/reflib/term_table.mli
+2 -2	metaprl/refiner/reflib/theory.ml
+1 -1	metaprl/refiner/reflib/theory.mli
+1 -1	metaprl/refiner/refsig/refine_error_sig.ml
+1 -1	metaprl/refiner/refsig/refine_sig.ml
+1 -1	metaprl/refiner/refsig/refiner_sig.ml
+1 -1	metaprl/refiner/refsig/resource.mlz
+1 -1	metaprl/refiner/refsig/rewrite_sig.ml
+1 -1	metaprl/refiner/refsig/term_addr_sig.ml
+1 -1	metaprl/refiner/refsig/term_base_sig.ml
+1 -1	metaprl/refiner/refsig/term_eval_sig.ml
+1 -1	metaprl/refiner/refsig/term_man_sig.ml
+1 -1	metaprl/refiner/refsig/term_meta_sig.ml
+7 -7	metaprl/refiner/refsig/term_op_sig.ml
+1 -1	metaprl/refiner/refsig/term_shape_sig.ml
+2 -2	metaprl/refiner/refsig/term_simple_sig.mlz
+1 -1	metaprl/refiner/refsig/term_subst_sig.ml
+1 -1	metaprl/refiner/refsig/termmod_sig.ml
+1 -1	metaprl/refiner/refsig/tm_base_sig.mlz
+1 -1	metaprl/refiner/refsig/tm_man_sig.mlz
+1 -1	metaprl/refiner/rewrite/rewrite.mlip
+3 -3	metaprl/refiner/rewrite/rewrite.mlp
+1 -1	metaprl/refiner/rewrite/rewrite_build_contractum.mlip
+11 -11	metaprl/refiner/rewrite/rewrite_build_contractum.mlp
+1 -1	metaprl/refiner/rewrite/rewrite_build_contractum_sig.mlz
+1 -1	metaprl/refiner/rewrite/rewrite_compile_contractum.mlip
+2 -2	metaprl/refiner/rewrite/rewrite_compile_contractum.mlp
+1 -1	metaprl/refiner/rewrite/rewrite_compile_contractum_sig.mlz
+1 -1	metaprl/refiner/rewrite/rewrite_compile_redex.mlip
+2 -2	metaprl/refiner/rewrite/rewrite_compile_redex.mlp
+1 -1	metaprl/refiner/rewrite/rewrite_compile_redex_sig.mlz
+1 -1	metaprl/refiner/rewrite/rewrite_debug.mlip
+4 -4	metaprl/refiner/rewrite/rewrite_debug.mlp
+1 -1	metaprl/refiner/rewrite/rewrite_debug_sig.ml
+1 -1	metaprl/refiner/rewrite/rewrite_match_redex.mlip
+3 -3	metaprl/refiner/rewrite/rewrite_match_redex.mlp
+1 -1	metaprl/refiner/rewrite/rewrite_match_redex_sig.mlz
+1 -1	metaprl/refiner/rewrite/rewrite_meta.mlip
+2 -2	metaprl/refiner/rewrite/rewrite_meta.mlp
+1 -1	metaprl/refiner/rewrite/rewrite_meta_sig.mlz
+1 -1	metaprl/refiner/rewrite/rewrite_type.mlip
+3 -3	metaprl/refiner/rewrite/rewrite_type.mlp
+3 -3	metaprl/refiner/rewrite/rewrite_type_sig.mlz
+1 -1	metaprl/refiner/rewrite/rewrite_util.mlip
+2 -2	metaprl/refiner/rewrite/rewrite_util.mlp
+1 -1	metaprl/refiner/rewrite/rewrite_util_sig.ml
+1 -1	metaprl/refiner/term_ds/term_addr_ds.mlip
+2 -2	metaprl/refiner/term_ds/term_addr_ds.mlp
+1 -1	metaprl/refiner/term_ds/term_base_ds.mlip
+2 -2	metaprl/refiner/term_ds/term_base_ds.mlp
+3 -3	metaprl/refiner/term_ds/term_ds.ml
+1 -1	metaprl/refiner/term_ds/term_ds.mli
+3 -3	metaprl/refiner/term_ds/term_ds_sig.ml
+1 -1	metaprl/refiner/term_ds/term_eval_ds.mlip
+1 -1	metaprl/refiner/term_ds/term_eval_ds.mlp
+1 -1	metaprl/refiner/term_ds/term_man_ds.mlip
+2 -2	metaprl/refiner/term_ds/term_man_ds.mlp
+1 -1	metaprl/refiner/term_ds/term_op_ds.mlip
+1 -1	metaprl/refiner/term_ds/term_op_ds.mlp
+1 -1	metaprl/refiner/term_ds/term_subst_ds.mlip
+3 -3	metaprl/refiner/term_ds/term_subst_ds.mlp
+1 -1	metaprl/refiner/term_gen/term_addr_gen.mlip
+1 -1	metaprl/refiner/term_gen/term_addr_gen.mlp
+1 -1	metaprl/refiner/term_gen/term_man_gen.mlip
+2 -2	metaprl/refiner/term_gen/term_man_gen.mlp
+1 -1	metaprl/refiner/term_gen/term_meta_gen.mlip
+1 -1	metaprl/refiner/term_gen/term_meta_gen.mlp
+1 -1	metaprl/refiner/term_gen/term_shape_gen.mlip
+1 -1	metaprl/refiner/term_gen/term_shape_gen.mlp
+1 -1	metaprl/refiner/term_std/term_base_std.mlip
+2 -2	metaprl/refiner/term_std/term_base_std.mlp
+1 -1	metaprl/refiner/term_std/term_eval_std.mlip
+1 -1	metaprl/refiner/term_std/term_eval_std.mlp
+1 -1	metaprl/refiner/term_std/term_op_std.mlip
+1 -1	metaprl/refiner/term_std/term_op_std.mlp
+3 -3	metaprl/refiner/term_std/term_std.ml
+1 -1	metaprl/refiner/term_std/term_std.mli
+2 -2	metaprl/refiner/term_std/term_std_sig.ml
+1 -1	metaprl/refiner/term_std/term_subst_std.mlip
+3 -3	metaprl/refiner/term_std/term_subst_std.mlp
+5 -5	metaprl/theories/base/base_auto_tactic.ml
+3 -3	metaprl/theories/base/base_auto_tactic.mli
+2 -2	metaprl/theories/base/base_cache.ml
+1 -1	metaprl/theories/base/base_cache.mli
+2 -2	metaprl/theories/base/base_dform.ml
+1 -1	metaprl/theories/base/base_dform.mli
+4 -4	metaprl/theories/base/base_dtactic.ml
+1 -1	metaprl/theories/base/base_dtactic.mli
+2 -2	metaprl/theories/base/base_rewrite.ml
+1 -1	metaprl/theories/base/base_rewrite.mli
+1 -1	metaprl/theories/base/base_theory.mlz
+2 -2	metaprl/theories/base/nuprl_font.ml
+1 -1	metaprl/theories/base/nuprl_font.mli
+2 -2	metaprl/theories/base/summary.ml
+1 -1	metaprl/theories/base/summary.mli
+3 -3	metaprl/theories/base/typeinf.ml
+1 -1	metaprl/theories/base/typeinf.mli
+1 -1	metaprl/theories/caml/caml_syntax.mli
+1 -1	metaprl/theories/czf/czf_all.mli
+1 -1	metaprl/theories/czf/czf_and.mli
+1 -1	metaprl/theories/czf/czf_equal.mli
+1 -1	metaprl/theories/czf/czf_exists.mli
+1 -1	metaprl/theories/czf/czf_false.mli
+1 -1	metaprl/theories/czf/czf_implies.mli
+3 -3	metaprl/theories/czf/czf_itt_all.ml
+1 -1	metaprl/theories/czf/czf_itt_all.mli
+3 -3	metaprl/theories/czf/czf_itt_and.ml
+1 -1	metaprl/theories/czf/czf_itt_and.mli
+2 -2	metaprl/theories/czf/czf_itt_axioms.ml
+1 -1	metaprl/theories/czf/czf_itt_axioms.mli
+3 -3	metaprl/theories/czf/czf_itt_dall.ml
+1 -1	metaprl/theories/czf/czf_itt_dall.mli
+3 -3	metaprl/theories/czf/czf_itt_dexists.ml
+1 -1	metaprl/theories/czf/czf_itt_dexists.mli
+3 -3	metaprl/theories/czf/czf_itt_empty.ml
+1 -1	metaprl/theories/czf/czf_itt_empty.mli
+3 -3	metaprl/theories/czf/czf_itt_eq.ml
+1 -1	metaprl/theories/czf/czf_itt_eq.mli
+2 -2	metaprl/theories/czf/czf_itt_eq_inner.ml
+1 -1	metaprl/theories/czf/czf_itt_eq_inner.mli
+3 -3	metaprl/theories/czf/czf_itt_exists.ml
+1 -1	metaprl/theories/czf/czf_itt_exists.mli
+3 -3	metaprl/theories/czf/czf_itt_false.ml
+1 -1	metaprl/theories/czf/czf_itt_false.mli
+3 -3	metaprl/theories/czf/czf_itt_implies.ml
+1 -1	metaprl/theories/czf/czf_itt_implies.mli
+1 -1	metaprl/theories/czf/czf_itt_isect.mli
+2 -2	metaprl/theories/czf/czf_itt_member.ml
+1 -1	metaprl/theories/czf/czf_itt_member.mli
+3 -3	metaprl/theories/czf/czf_itt_or.ml
+1 -1	metaprl/theories/czf/czf_itt_or.mli
+3 -3	metaprl/theories/czf/czf_itt_pre_set.ml
+1 -1	metaprl/theories/czf/czf_itt_pre_set.mli
+2 -2	metaprl/theories/czf/czf_itt_rel.ml
+1 -1	metaprl/theories/czf/czf_itt_rel.mli
+1 -1	metaprl/theories/czf/czf_itt_res.ml
+1 -1	metaprl/theories/czf/czf_itt_res.mli
+3 -3	metaprl/theories/czf/czf_itt_sall.ml
+1 -1	metaprl/theories/czf/czf_itt_sall.mli
+3 -3	metaprl/theories/czf/czf_itt_sep.ml
+1 -1	metaprl/theories/czf/czf_itt_sep.mli
+4 -4	metaprl/theories/czf/czf_itt_set.ml
+1 -1	metaprl/theories/czf/czf_itt_set.mli
+3 -3	metaprl/theories/czf/czf_itt_set_ext.ml
+1 -1	metaprl/theories/czf/czf_itt_set_ext.mli
+3 -3	metaprl/theories/czf/czf_itt_set_ind.ml
+1 -1	metaprl/theories/czf/czf_itt_set_ind.mli
+3 -3	metaprl/theories/czf/czf_itt_sexists.ml
+1 -1	metaprl/theories/czf/czf_itt_sexists.mli
+3 -3	metaprl/theories/czf/czf_itt_small.ml
+1 -1	metaprl/theories/czf/czf_itt_small.mli
+3 -3	metaprl/theories/czf/czf_itt_true.ml
+1 -1	metaprl/theories/czf/czf_itt_true.mli
+3 -3	metaprl/theories/czf/czf_itt_union.ml
+1 -1	metaprl/theories/czf/czf_itt_union.mli
+1 -1	metaprl/theories/czf/czf_member.mli
+1 -1	metaprl/theories/czf/czf_or.mli
+1 -1	metaprl/theories/czf/czf_set.ml
+1 -1	metaprl/theories/czf/czf_set.mli
+1 -1	metaprl/theories/czf/czf_struct.mli
+1 -1	metaprl/theories/czf/czf_theory.mli
+1 -1	metaprl/theories/czf/czf_true.ml
+1 -1	metaprl/theories/czf/czf_true.mli
+1 -1	metaprl/theories/czf/czf_wf.ml
+1 -1	metaprl/theories/czf/czf_wf.mli
+1 -1	metaprl/theories/fol/fol_all.ml
+1 -1	metaprl/theories/fol/fol_and.ml
+1 -1	metaprl/theories/fol/fol_exists.ml
+1 -1	metaprl/theories/fol/fol_false.ml
+1 -1	metaprl/theories/fol/fol_implies.ml
+1 -1	metaprl/theories/fol/fol_not.ml
+1 -1	metaprl/theories/fol/fol_or.ml
+1 -1	metaprl/theories/fol/fol_struct.ml
+1 -1	metaprl/theories/fol/fol_true.ml
+1 -1	metaprl/theories/fol/fol_univ.ml
+11 -11	metaprl/theories/itt/itt_arith.ml
+1 -1	metaprl/theories/itt/itt_arith.mli
+3 -3	metaprl/theories/itt/itt_atom.ml
+1 -1	metaprl/theories/itt/itt_atom.mli
+2 -2	metaprl/theories/itt/itt_bool.ml
+1 -1	metaprl/theories/itt/itt_bool.mli
+3 -3	metaprl/theories/itt/itt_derive.ml
+1 -1	metaprl/theories/itt/itt_derive.mli
+3 -3	metaprl/theories/itt/itt_dfun.ml
+1 -1	metaprl/theories/itt/itt_dfun.mli
+3 -3	metaprl/theories/itt/itt_dprod.ml
+1 -1	metaprl/theories/itt/itt_dprod.mli
+4 -4	metaprl/theories/itt/itt_equal.ml
+1 -1	metaprl/theories/itt/itt_equal.mli
+2 -2	metaprl/theories/itt/itt_ext_equal.ml
+1 -1	metaprl/theories/itt/itt_ext_equal.mli
+3 -3	metaprl/theories/itt/itt_fun.ml
+1 -1	metaprl/theories/itt/itt_fun.mli
+3 -3	metaprl/theories/itt/itt_int.ml
+3 -3	metaprl/theories/itt/itt_int.mli
+1 -1	metaprl/theories/itt/itt_int_bool.ml
+1 -1	metaprl/theories/itt/itt_int_bool.mli
+3 -3	metaprl/theories/itt/itt_isect.ml
+1 -1	metaprl/theories/itt/itt_isect.mli
+3 -3	metaprl/theories/itt/itt_list.ml
+1 -1	metaprl/theories/itt/itt_list.mli
+4 -4	metaprl/theories/itt/itt_logic.ml
+1 -1	metaprl/theories/itt/itt_logic.mli
+3 -3	metaprl/theories/itt/itt_prec.ml
+1 -1	metaprl/theories/itt/itt_prec.mli
+3 -3	metaprl/theories/itt/itt_prod.ml
+1 -1	metaprl/theories/itt/itt_prod.mli
+2 -2	metaprl/theories/itt/itt_prop_decide.ml
+1 -1	metaprl/theories/itt/itt_prop_decide.mli
+3 -3	metaprl/theories/itt/itt_quotient.ml
+1 -1	metaprl/theories/itt/itt_quotient.mli
+3 -3	metaprl/theories/itt/itt_rfun.ml
+1 -1	metaprl/theories/itt/itt_rfun.mli
+3 -3	metaprl/theories/itt/itt_set.ml
+1 -1	metaprl/theories/itt/itt_set.mli
+3 -3	metaprl/theories/itt/itt_squash.ml
+1 -1	metaprl/theories/itt/itt_squash.mli
+3 -3	metaprl/theories/itt/itt_srec.ml
+1 -1	metaprl/theories/itt/itt_srec.mli
+4 -4	metaprl/theories/itt/itt_struct.ml
+1 -1	metaprl/theories/itt/itt_struct.mli
+3 -3	metaprl/theories/itt/itt_subtype.ml
+1 -1	metaprl/theories/itt/itt_subtype.mli
+3 -3	metaprl/theories/itt/itt_test.ml
+1 -1	metaprl/theories/itt/itt_test.mli
+1 -1	metaprl/theories/itt/itt_theory.ml
+1 -1	metaprl/theories/itt/itt_theory.mli
+3 -3	metaprl/theories/itt/itt_union.ml
+1 -1	metaprl/theories/itt/itt_union.mli
+3 -3	metaprl/theories/itt/itt_unit.ml
+1 -1	metaprl/theories/itt/itt_unit.mli
+3 -3	metaprl/theories/itt/itt_void.ml
+1 -1	metaprl/theories/itt/itt_void.mli
+2 -2	metaprl/theories/itt/itt_w.ml
+1 -1	metaprl/theories/itt/itt_w.mli
+2 -2	metaprl/theories/itt/main.ml
+1 -1	metaprl/theories/itt/main.mli
+1 -1	metaprl/theories/itt/test.ml
+1 -1	metaprl/theories/itt/test.mli
+1 -1	metaprl/theories/lf/lf_ctx.mli
+1 -1	metaprl/theories/lf/lf_dfun.mli
+1 -1	metaprl/theories/lf/lf_kind.mli
+1 -1	metaprl/theories/lf/lf_sig.mli
+1 -1	metaprl/theories/lf/lf_type.mli
+2 -2	metaprl/theories/lf/main.ml
+1 -1	metaprl/theories/ocaml/ocaml.mlz
+2 -2	metaprl/theories/ocaml/ocaml_base_df.ml
+1 -1	metaprl/theories/ocaml/ocaml_base_df.mli
+1 -1	metaprl/theories/ocaml/ocaml_df.mlz
+2 -2	metaprl/theories/ocaml/ocaml_expr_df.ml
+1 -1	metaprl/theories/ocaml/ocaml_expr_df.mli
+2 -2	metaprl/theories/ocaml/ocaml_me_df.ml
+1 -1	metaprl/theories/ocaml/ocaml_me_df.mli
+2 -2	metaprl/theories/ocaml/ocaml_mt_df.ml
+1 -1	metaprl/theories/ocaml/ocaml_mt_df.mli
+2 -2	metaprl/theories/ocaml/ocaml_patt_df.ml
+1 -1	metaprl/theories/ocaml/ocaml_patt_df.mli
+2 -2	metaprl/theories/ocaml/ocaml_sig_df.ml
+1 -1	metaprl/theories/ocaml/ocaml_sig_df.mli
+2 -2	metaprl/theories/ocaml/ocaml_str_df.ml
+1 -1	metaprl/theories/ocaml/ocaml_str_df.mli
+2 -2	metaprl/theories/ocaml/ocaml_type_df.ml
+1 -1	metaprl/theories/ocaml/ocaml_type_df.mli
+2 -2	metaprl/theories/ocaml_sos/ocaml_base_sos.ml
+1 -1	metaprl/theories/ocaml_sos/ocaml_base_sos.mli
+2 -2	metaprl/theories/ocaml_sos/ocaml_expr_sos.ml
+1 -1	metaprl/theories/ocaml_sos/ocaml_expr_sos.mli
+2 -2	metaprl/theories/ocaml_sos/ocaml_logic.ml
+1 -1	metaprl/theories/ocaml_sos/ocaml_logic.mli
+2 -2	metaprl/theories/ocaml_sos/ocaml_me_sos.ml
+1 -1	metaprl/theories/ocaml_sos/ocaml_me_sos.mli
+2 -2	metaprl/theories/ocaml_sos/ocaml_mt_sos.ml
+1 -1	metaprl/theories/ocaml_sos/ocaml_mt_sos.mli
+2 -2	metaprl/theories/ocaml_sos/ocaml_patt_sos.ml
+1 -1	metaprl/theories/ocaml_sos/ocaml_patt_sos.mli
+2 -2	metaprl/theories/ocaml_sos/ocaml_sig_sos.ml
+1 -1	metaprl/theories/ocaml_sos/ocaml_sig_sos.mli
+2 -2	metaprl/theories/ocaml_sos/ocaml_str_sos.ml
+1 -1	metaprl/theories/ocaml_sos/ocaml_str_sos.mli
+1 -1	metaprl/theories/ocaml_sos/ocaml_theory.mlz
+2 -2	metaprl/theories/ocaml_sos/ocaml_type_sos.ml
+1 -1	metaprl/theories/ocaml_sos/ocaml_type_sos.mli
+2 -2	metaprl/theories/rewrite/rw_beta.ml
+1 -1	metaprl/theories/rewrite/rw_beta.mli
+1 -1	metaprl/theories/tactic/Makefile
+3 -3	metaprl/theories/tactic/conversionals.ml
+2 -2	metaprl/theories/tactic/conversionals.mli
Added	metaprl/theories/tactic/mptop.ml
Properties	metaprl/theories/tactic/mptop.ml
Added	metaprl/theories/tactic/mptop.mli
Properties	metaprl/theories/tactic/mptop.mli
Deleted	metaprl/theories/tactic/nltop.ml
Deleted	metaprl/theories/tactic/nltop.mli
+2 -2	metaprl/theories/tactic/perv.ml
+1 -1	metaprl/theories/tactic/perv.mli
+1 -1	metaprl/theories/tactic/remote_null.ml
+1 -1	metaprl/theories/tactic/remote_null.mli
+1 -1	metaprl/theories/tactic/remote_sig.mlz
+2 -2	metaprl/theories/tactic/rewrite_type.ml
+1 -1	metaprl/theories/tactic/rewrite_type.mli
+2 -2	metaprl/theories/tactic/sequent.ml
+1 -1	metaprl/theories/tactic/sequent.mli
+2 -2	metaprl/theories/tactic/tactic_cache.ml
+1 -1	metaprl/theories/tactic/tactic_cache.mli
+2 -2	metaprl/theories/tactic/tactic_type.ml
+2 -2	metaprl/theories/tactic/tactic_type.mli
+3 -3	metaprl/theories/tactic/tacticals.ml
+2 -2	metaprl/theories/tactic/tacticals.mli
+2 -2	metaprl/theories/tactic/var.ml
+1 -1	metaprl/theories/tactic/var.mli
+2 -2	metaprl/theories/tptp/tptp.ml
+1 -1	metaprl/theories/tptp/tptp.mli
+2 -2	metaprl/theories/tptp/tptp_cache.ml
+1 -1	metaprl/theories/tptp/tptp_cache.mli
+1 -1	metaprl/theories/tptp/tptp_lex.mli
+3 -3	metaprl/theories/tptp/tptp_load.ml
+1 -1	metaprl/theories/tptp/tptp_load.mli
+2 -2	metaprl/theories/tptp/tptp_prove.ml
+1 -1	metaprl/theories/tptp/tptp_prove.mli
+1 -1	metaprl/theories/tptp/tptp_type.mlz