Commit log for MetaPRL

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-06-01 06:57:13 -0700 (Mon, 01 Jun 1998)
Revision: 2209
Log message:

Proving twice one is two.

Changes	Path
+4 -5	metaprl/editor/ml/Makefile
+4 -2	metaprl/editor/ml/io_proof.ml
+3 -1	metaprl/editor/ml/io_proof_type.mlz
+1 -0	metaprl/editor/ml/make1
+6 -3	metaprl/editor/ml/nl
+3 -25	metaprl/editor/ml/package_info.ml
+3 -1	metaprl/editor/ml/package_info.mli
+4 -2	metaprl/editor/ml/package_int.ml
+3 -10	metaprl/editor/ml/package_type.mlz
+3 -4	metaprl/editor/ml/proof.ml
+3 -1	metaprl/editor/ml/proof_edit.ml
+4 -1	metaprl/editor/ml/proof_step.ml
+3 -1	metaprl/editor/ml/proof_step.mli
+72 -53	metaprl/editor/ml/shell.ml
+4 -2	metaprl/editor/ml/shell.mli
+140 -15	metaprl/editor/ml/shell_p4.ml
+7 -0	metaprl/editor/ml/shell_p4.mli
+18 -4	metaprl/editor/ml/shell_rewrite.ml
+3 -1	metaprl/editor/ml/shell_type.mlz
+7 -9	metaprl/editor/ml/test.ml
+6 -2	metaprl/editor/ml/test.mli
+55 -48	metaprl/filter/Makefile
+3 -2	metaprl/filter/buffer.ml
+3 -3	metaprl/filter/filter_bin.ml
+3 -8	metaprl/filter/filter_cache.ml
+3 -2	metaprl/filter/filter_cache.mli
+6 -19	metaprl/filter/filter_cache_fun.ml
+3 -1	metaprl/filter/filter_cache_fun.mli
+4 -6	metaprl/filter/filter_comment.ml
+4 -0	metaprl/filter/filter_exn.ml
+4 -2	metaprl/filter/filter_hash.ml
+4 -2	metaprl/filter/filter_html.ml
+3 -10	metaprl/filter/filter_ocaml.ml
+5 -65	metaprl/filter/filter_parse.ml
+17 -64	metaprl/filter/filter_prog.ml
+3 -1	metaprl/filter/filter_prog.mli
+5 -17	metaprl/filter/filter_summary.ml
+3 -20	metaprl/filter/filter_summary_io.ml
+3 -7	metaprl/filter/filter_summary_type.mlz
+4 -1	metaprl/filter/filter_type.mlz
+3 -2	metaprl/filter/infix.pre.ml
+3 -8	metaprl/filter/mLast_util.ml
+36 -14	metaprl/filter/prlcomp.ml
+4 -114	metaprl/filter/term_grammar.ml
+3 -1	metaprl/filter/term_quote.ml
+3 -24	metaprl/filter/test_gram.ml
+6 -20	metaprl/horus/term.ml
+3 -2	metaprl/horus/term.mli
+16 -19	metaprl/library/ascii_scan.ml
+3 -3	metaprl/library/ascii_scan.mli
+41 -43	metaprl/library/basic.ml
+1 -3	metaprl/library/basic.mli
+2 -3	metaprl/library/bigInt.ml
+78 -96	metaprl/library/db.ml
+51 -58	metaprl/library/definition.ml
+4 -4	metaprl/library/definition.mli
+2 -3	metaprl/library/int32.ml
+1 -1	metaprl/library/int32.mli
+47 -52	metaprl/library/library.ml
+18 -19	metaprl/library/library.mli
+4 -6	metaprl/library/library_eval.ml
+1 -1	metaprl/library/library_eval.mli
+5 -9	metaprl/library/link.ml
+1 -1	metaprl/library/link.mli
+52 -85	metaprl/library/mathBus.ml
+2 -3	metaprl/library/mathBus.mli
+24 -27	metaprl/library/mbterm.ml
+1 -1	metaprl/library/mbterm.mli
+0 -1	metaprl/library/nuprl5.ml
+1 -1	metaprl/library/object_id.ml
+1 -1	metaprl/library/object_id.mli
+2 -2	metaprl/library/oidtable.ml
+0 -1	metaprl/library/oidtable.mli
+76 -90	metaprl/library/orb.ml
+1 -2	metaprl/library/orb.mli
+8 -12	metaprl/library/registry.ml
+2 -3	metaprl/library/registry.mli
+7 -7	metaprl/library/socketIo.ml
+0 -1	metaprl/library/socketIo.mli
+15 -22	metaprl/library/tentfunctor.ml
+43 -49	metaprl/library/test.ml
+0 -1	metaprl/library/test.mli
+11 -15	metaprl/library/utils.ml
+2 -2	metaprl/library/utils.mli
+54 -48	metaprl/mk/config
+3 -1	metaprl/mllib/ctype.mli
+3 -4	metaprl/mllib/dag.mlz
+4 -1	metaprl/mllib/debug_set.ml
+6 -5	metaprl/mllib/env_arg.ml
+3 -20	metaprl/mllib/file_base.ml
+3 -7	metaprl/mllib/file_base_type.ml
+3 -4	metaprl/mllib/file_type_base.ml
+3 -27	metaprl/mllib/imp_dag.ml
+15 -12	metaprl/mllib/list_util.ml
+4 -1	metaprl/mllib/string_util.ml
+3 -1	metaprl/refiner/refbase/opname.ml
+30 -8	metaprl/refiner/refiner/rewrite.ml
+23 -8	metaprl/refiner/reflib/dform.ml
+3 -1	metaprl/refiner/reflib/dform.mli
+3 -1	metaprl/refiner/reflib/dform_print.ml
+3 -5	metaprl/refiner/reflib/ml_file.ml
+3 -45	metaprl/refiner/reflib/ml_format.ml
+3 -7	metaprl/refiner/reflib/ml_print.ml
+3 -5	metaprl/refiner/reflib/ml_print_sig.mlz
+3 -2	metaprl/refiner/reflib/ml_string.ml
+4 -5	metaprl/refiner/reflib/rformat.ml
+4 -5	metaprl/refiner/reflib/term_dtable.ml
+4 -3	metaprl/refiner/reflib/term_stable.ml
+3 -1	metaprl/refiner/reflib/term_table.ml
+4 -1	metaprl/refiner/reflib/term_template.ml
+3 -12	metaprl/refiner/refsig/rewrite_sig.ml
+3 -1	metaprl/refiner/refsig/term_addr_sig.ml
+3 -13	metaprl/refiner/refsig/term_man_sig.ml
+3 -1	metaprl/refiner/refsig/term_meta_sig.ml
+3 -20	metaprl/refiner/refsig/term_op_sig.ml
+3 -3	metaprl/refiner/refsig/term_sig.ml
+3 -3	metaprl/refiner/refsig/term_subst_sig.ml
+29 -29	metaprl/refiner/term_ds/term_ds.ml
+5 -5	metaprl/refiner/term_ds/term_ds.mli
+44 -44	metaprl/refiner/term_ds/term_op_ds.ml
+5 -2	metaprl/refiner/term_gen/term_meta_gen.ml
+5 -2	metaprl/refiner/term_gen/term_meta_gen.mli
+8 -2	metaprl/refiner/term_std/term_addr_std.ml
+16 -4	metaprl/refiner/term_std/term_man_std.ml
+6 -3	metaprl/refiner/term_std/term_std.ml
+3 -2	metaprl/theories/base/base_cache.ml
+15 -3	metaprl/theories/base/base_dform.ml
+21 -17	metaprl/theories/base/base_dform.mli
+4 -5	metaprl/theories/base/base_dtactic.ml
+28 -30	metaprl/theories/base/evaluator.ml
+3 -3	metaprl/theories/base/typeinf.ml
+3 -1	metaprl/theories/base/typeinf.mli
+4 -1	metaprl/theories/czf/czf_struct.mli
+10 -6	metaprl/theories/itt/itt_atom.ml
+6 -1	metaprl/theories/itt/itt_dfun.ml
+14 -8	metaprl/theories/itt/itt_dprod.ml
+18 -14	metaprl/theories/itt/itt_equal.ml
+3 -2	metaprl/theories/itt/itt_equal.mli
+6 -1	metaprl/theories/itt/itt_fun.ml
+23 -21	metaprl/theories/itt/itt_int.ml
+9 -3	metaprl/theories/itt/itt_isect.ml
+10 -7	metaprl/theories/itt/itt_list.ml
+3 -1	metaprl/theories/itt/itt_list.mli
+21 -28	metaprl/theories/itt/itt_logic.ml
+4 -1	metaprl/theories/itt/itt_prec.ml
+4 -1	metaprl/theories/itt/itt_prec.mli
+9 -3	metaprl/theories/itt/itt_prod.ml
+4 -1	metaprl/theories/itt/itt_prod.mli
+10 -5	metaprl/theories/itt/itt_quotient.ml
+4 -1	metaprl/theories/itt/itt_quotient.mli
+14 -14	metaprl/theories/itt/itt_redrules.ml
+15 -9	metaprl/theories/itt/itt_rfun.ml
+12 -9	metaprl/theories/itt/itt_set.ml
+7 -3	metaprl/theories/itt/itt_soft.ml
+5 -2	metaprl/theories/itt/itt_soft.mli
+4 -4	metaprl/theories/itt/itt_squash.ml
+3 -1	metaprl/theories/itt/itt_squash.mli
+9 -5	metaprl/theories/itt/itt_srec.ml
+9 -6	metaprl/theories/itt/itt_srec.mli
+9 -2	metaprl/theories/itt/itt_struct.ml
+8 -6	metaprl/theories/itt/itt_subtype.ml
+3 -1	metaprl/theories/itt/itt_subtype.mli
+8 -1	metaprl/theories/itt/itt_union.ml
+4 -1	metaprl/theories/itt/itt_union.mli
+5 -1	metaprl/theories/itt/itt_unit.ml
+5 -1	metaprl/theories/itt/itt_void.ml
+3 -1	metaprl/theories/lf/lf_ctx.mli
+3 -2	metaprl/theories/lf/lf_sig.mli
+3 -8	metaprl/theories/ocaml/ocaml.mlz
+2 -2	metaprl/theories/ocaml/ocaml_df.ml
+2 -2	metaprl/theories/ocaml/ocaml_df.mli
+3 -1	metaprl/theories/ocaml/ocaml_expr_df.ml
+3 -2	metaprl/theories/ocaml/ocaml_patt_df.ml
+4 -1	metaprl/theories/ocaml/ocaml_str_df.ml
+3 -1	metaprl/theories/ocaml/ocaml_type_df.ml
+4 -1	metaprl/theories/ocaml_sos/ocaml_base_sos.ml
+4 -1	metaprl/theories/ocaml_sos/ocaml_base_sos.mli
+7 -13	metaprl/theories/ocaml_sos/ocaml_expr_sos.ml
+8 -14	metaprl/theories/ocaml_sos/ocaml_expr_sos.mli
+3 -4	metaprl/theories/ocaml_sos/ocaml_patt_sos.ml
+3 -4	metaprl/theories/ocaml_sos/ocaml_patt_sos.mli
+3 -3	metaprl/theories/rewrite/rw_beta.ml
+6 -33	metaprl/theories/tactic/tactic_cache.ml
+3 -1	metaprl/theories/tactic/tactic_cache.mli
+5 -2	metaprl/theories/tactic/tactic_type.mlz
+4 -4	metaprl/theories/tactic/tacticals.ml
Properties	metaprl/util
+4 -2	metaprl/util/Makefile
+1 -1	metaprl/util/misc.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-06-01 12:29:16 -0700 (Mon, 01 Jun 1998)
Revision: 2210
Log message:

*** empty log message ***

Changes	Path
+1 -0	metaprl/Makefile

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-06-01 12:54:01 -0700 (Mon, 01 Jun 1998)
Revision: 2211
Log message:

Working addition proof. Removing polymorphism from refiner(?)

Changes	Path
+4 -1	metaprl/editor/ml/proof_edit.ml
+127 -39	metaprl/editor/ml/shell_p4.ml
+4 -1	metaprl/editor/ml/test.ml
+7 -0	metaprl/filter/filter_parse.ml
+2 -2	metaprl/refiner/Makefile
+16 -0	metaprl/refiner/refiner/refine.ml
+5 -0	metaprl/refiner/refiner/rewrite.ml
+10 -2	metaprl/refiner/refsig/refine_sig.ml
+4 -0	metaprl/refiner/refsig/term_sig.ml
+3 -0	metaprl/refiner/term_ds/term_ds.ml
+1 -0	metaprl/refiner/term_ds/term_ds.mli
+19 -4	metaprl/refiner/term_std/term_addr_std.ml
+6 -0	metaprl/refiner/term_std/term_std.ml
+4 -0	metaprl/refiner/term_std/term_std.mli
+1 -0	metaprl/theories/base/Makefile
Added	metaprl/theories/base/base_rewrite.ml
Properties	metaprl/theories/base/base_rewrite.ml
Added	metaprl/theories/base/base_rewrite.mli
Properties	metaprl/theories/base/base_rewrite.mli
+4 -0	metaprl/theories/tactic/tactic_type.mlz

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-02 14:52:00 -0700 (Tue, 02 Jun 1998)
Revision: 2212
Log message:

Use == for comparing opnames

Changes	Path
+1 -1	metaprl/refiner/term_ds/term_ds.ml
+24 -24	metaprl/refiner/term_ds/term_op_ds.ml
+24 -21	metaprl/refiner/term_std/term_op_std.ml
+4 -1	metaprl/refiner/term_std/term_std.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-02 15:22:11 -0700 (Tue, 02 Jun 1998)
Revision: 2213
Log message:

Refiner lib depends on term_* .mli files

Changes	Path
+2 -1	metaprl/refiner/Makefile

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-06-03 08:23:59 -0700 (Wed, 03 Jun 1998)
Revision: 2214
Log message:

Generalized many the term_addr, term_man, and term_shape modules.

Changes	Path
+99 -33	metaprl/refiner/Makefile
+118 -294	metaprl/refiner/refiner/refine.ml
+6 -3	metaprl/refiner/refiner/refiner_ds.ml
+6 -3	metaprl/refiner/refiner/refiner_std.ml
Properties	metaprl/refiner/refsig
+1 -0	metaprl/refiner/refsig/Files
+17 -0	metaprl/refiner/refsig/Makefile
+28 -57	metaprl/refiner/refsig/refine_sig.ml
+6 -1	metaprl/refiner/refsig/term_addr_sig.ml
+3 -1	metaprl/refiner/refsig/term_man_sig.ml
Deleted	metaprl/refiner/refsig/term_sig.ml
Added	metaprl/refiner/refsig/term_simple_sig.mlz
Properties	metaprl/refiner/refsig/term_simple_sig.mlz
+0 -3	metaprl/refiner/term_ds/Files
Deleted	metaprl/refiner/term_ds/term_addr_ds.ml
Deleted	metaprl/refiner/term_ds/term_addr_ds.mli
Deleted	metaprl/refiner/term_ds/term_man_ds.ml
Deleted	metaprl/refiner/term_ds/term_man_ds.mli
Deleted	metaprl/refiner/term_ds/term_shape_ds.ml
Deleted	metaprl/refiner/term_ds/term_shape_ds.mli
+1 -0	metaprl/refiner/term_ds/term_subst_ds.ml
+3 -0	metaprl/refiner/term_gen/Files
Added	metaprl/refiner/term_gen/term_addr_gen.ml
Properties	metaprl/refiner/term_gen/term_addr_gen.ml
Added	metaprl/refiner/term_gen/term_addr_gen.mli
Properties	metaprl/refiner/term_gen/term_addr_gen.mli
Added	metaprl/refiner/term_gen/term_man_gen.ml
Properties	metaprl/refiner/term_gen/term_man_gen.ml
Added	metaprl/refiner/term_gen/term_man_gen.mli
Properties	metaprl/refiner/term_gen/term_man_gen.mli
Added	metaprl/refiner/term_gen/term_shape_gen.ml
Properties	metaprl/refiner/term_gen/term_shape_gen.ml
Added	metaprl/refiner/term_gen/term_shape_gen.mli
Properties	metaprl/refiner/term_gen/term_shape_gen.mli
+1 -4	metaprl/refiner/term_std/Files
Deleted	metaprl/refiner/term_std/term_addr_std.ml
Deleted	metaprl/refiner/term_std/term_addr_std.mli
Deleted	metaprl/refiner/term_std/term_man_std.ml
Deleted	metaprl/refiner/term_std/term_man_std.mli
Deleted	metaprl/refiner/term_std/term_shape_std.ml
Deleted	metaprl/refiner/term_std/term_shape_std.mli
+18 -2	metaprl/refiner/term_std/term_std.ml
+5 -0	metaprl/refiner/term_std/term_std.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-03 13:08:58 -0700 (Wed, 03 Jun 1998)
Revision: 2215
Log message:

Fixed dependencies

Changes	Path
+2 -2	metaprl/refiner/Makefile

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-06-03 15:20:09 -0700 (Wed, 03 Jun 1998)
Revision: 2216
Log message:

Nonpolymorphic refiner.

Changes	Path
+1 -0	metaprl/clib/Makefile
Added	metaprl/clib/execvp.c
Properties	metaprl/clib/execvp.c
+5 -0	metaprl/clib/punix.ml
+8 -0	metaprl/clib/punix.mli
+20 -50	metaprl/editor/ml/io_proof.ml
+10 -6	metaprl/editor/ml/io_proof_type.mlz
+30 -30	metaprl/editor/ml/proof.ml
+8 -4	metaprl/editor/ml/proof_edit.ml
+28 -27	metaprl/editor/ml/proof_step.ml
+7 -9	metaprl/editor/ml/shell_rewrite.ml
+20 -9	metaprl/filter/filter_prog.ml
+4 -1	metaprl/filter/prlcomp.ml
+16 -0	metaprl/mllib/list_util.ml
+4 -0	metaprl/mllib/list_util.mli
+4 -1	metaprl/refiner/refiner/refiner_ds.ml
+4 -1	metaprl/refiner/refiner/refiner_std.ml
+6 -2	metaprl/refiner/refsig/refiner_sig.ml
+9 -6	metaprl/refiner/refsig/term_addr_sig.ml
+13 -3	metaprl/refiner/refsig/term_man_sig.ml
+14 -0	metaprl/refiner/refsig/term_simple_sig.mlz
+3 -0	metaprl/refiner/term_ds/term_ds.ml
+1 -0	metaprl/refiner/term_ds/term_ds.mli
+12 -13	metaprl/refiner/term_gen/term_addr_gen.ml
+285 -155	metaprl/refiner/term_gen/term_man_gen.ml
+7 -0	metaprl/refiner/term_gen/term_man_gen.mli
+6 -2	metaprl/refiner/term_std/term_std.ml
+4 -0	metaprl/refiner/term_std/term_std.mli
+6 -3	metaprl/theories/base/base_cache.ml
+6 -3	metaprl/theories/base/base_cache.mli
+6 -1	metaprl/theories/base/typeinf.ml
+6 -1	metaprl/theories/itt/itt_equal.ml
+9 -11	metaprl/theories/itt/itt_soft.ml
+4 -1	metaprl/theories/itt/itt_soft.mli
+8 -3	metaprl/theories/itt/itt_squash.ml
+6 -1	metaprl/theories/itt/itt_subtype.ml
+4 -5	metaprl/theories/tactic/Makefile
Added	metaprl/theories/tactic/conversionals.ml
Properties	metaprl/theories/tactic/conversionals.ml
Added	metaprl/theories/tactic/conversionals.mli
Properties	metaprl/theories/tactic/conversionals.mli
Added	metaprl/theories/tactic/rewrite_type.ml
Properties	metaprl/theories/tactic/rewrite_type.ml
Added	metaprl/theories/tactic/rewrite_type.mli
Properties	metaprl/theories/tactic/rewrite_type.mli
+45 -22	metaprl/theories/tactic/sequent.ml
+26 -17	metaprl/theories/tactic/sequent.mli
Added	metaprl/theories/tactic/tactic_type.ml
Properties	metaprl/theories/tactic/tactic_type.ml
Added	metaprl/theories/tactic/tactic_type.mli
Properties	metaprl/theories/tactic/tactic_type.mli
Deleted	metaprl/theories/tactic/tactic_type.mlz
+62 -96	metaprl/theories/tactic/tacticals.ml
+32 -29	metaprl/theories/tactic/tacticals.mli
+22 -20	metaprl/theories/tactic/var.ml
+9 -7	metaprl/theories/tactic/var.mli
+11 -2	metaprl/util/ocamldep.mll

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-04 12:52:56 -0700 (Thu, 04 Jun 1998)
Revision: 2217
Log message:

Efficiency

Changes	Path
+9 -0	metaprl/mllib/list_util.ml
+4 -0	metaprl/mllib/list_util.mli
+26 -18	metaprl/refiner/term_ds/term_ds.ml
+1 -0	metaprl/refiner/term_ds/term_ds.mli
+2 -3	metaprl/refiner/term_ds/term_subst_ds.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-05 14:11:10 -0700 (Fri, 05 Jun 1998)
Revision: 2218
Log message:

Changes	Path
+1 -1	metaprl/lib/Makefile

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-05 14:15:34 -0700 (Fri, 05 Jun 1998)
Revision: 2219
Log message:

Clean should also remove generated .ml & .mli files

Changes	Path
+2 -0	metaprl/filter/Makefile

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-05 19:31:54 -0700 (Fri, 05 Jun 1998)
Revision: 2220
Log message:

      Commented out the parts of the code that are not compatible
      with the Camlp4 1.07.02+1

Changes	Path
+8 -4	metaprl/filter/filter_comment.ml
+12 -8	metaprl/filter/filter_hash.ml
+24 -12	metaprl/filter/filter_ocaml.ml
+12 -8	metaprl/filter/mLast_util.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-06 18:08:40 -0700 (Sat, 06 Jun 1998)
Revision: 2221
Log message:

      Use the sets implementation based on the splay trees in Term_ds module
      This implementation is based on the splay trees code taken from TAL typechecker

Changes	Path
+2 -1	metaprl/mllib/Makefile
Added	metaprl/mllib/splay_set.ml
Properties	metaprl/mllib/splay_set.ml
Added	metaprl/mllib/splay_set.mli
Properties	metaprl/mllib/splay_set.mli
+10 -10	metaprl/refiner/term_ds/term_ds.ml
+1 -1	metaprl/refiner/term_ds/term_ds.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-06-09 13:53:04 -0700 (Tue, 09 Jun 1998)
Revision: 2222
Log message:

      Propagated refinement changes.
      New tacticals module.

Changes	Path
Properties	metaprl/editor/ml
+2 -0	metaprl/editor/ml/Makefile
+72 -40	metaprl/editor/ml/io_proof.ml
+7 -3	metaprl/editor/ml/io_proof_type.mlz
+8 -2	metaprl/editor/ml/package_info.ml
+8 -1	metaprl/editor/ml/package_info.mli
+6 -0	metaprl/editor/ml/package_type.mlz
+12 -13	metaprl/editor/ml/proof.ml
+6 -0	metaprl/editor/ml/proof.mli
+11 -14	metaprl/editor/ml/proof_step.ml
+6 -0	metaprl/editor/ml/proof_step.mli
Added	metaprl/editor/ml/proof_type.mlz
Properties	metaprl/editor/ml/proof_type.mlz
+11 -3	metaprl/editor/ml/shell_rewrite.ml
Added	metaprl/editor/ml/x.ml
Properties	metaprl/editor/ml/x.ml
+9 -5	metaprl/filter/filter_prog.ml
+10 -89	metaprl/refiner/Makefile
+0 -1	metaprl/refiner/reflib/Files
+10 -5	metaprl/refiner/reflib/term_dtable.ml
+70 -154	metaprl/refiner/reflib/term_stable.ml
+14 -11	metaprl/refiner/reflib/term_stable.mli
Deleted	metaprl/refiner/reflib/term_template.ml
Deleted	metaprl/refiner/reflib/term_template.mli
+4 -3	metaprl/refiner/refsig/refine_sig.ml
+16 -1	metaprl/refiner/refsig/term_man_sig.ml
+84 -37	metaprl/refiner/term_gen/term_man_gen.ml
+5 -1	metaprl/theories/base/base_dtactic.ml
+5 -1	metaprl/theories/base/typeinf.ml
+26 -21	metaprl/theories/itt/itt_dfun.ml
+9 -6	metaprl/theories/itt/itt_dprod.ml
+5 -1	metaprl/theories/itt/itt_equal.ml
+7 -4	metaprl/theories/itt/itt_fun.ml
+7 -4	metaprl/theories/itt/itt_int.ml
+8 -5	metaprl/theories/itt/itt_isect.ml
+7 -4	metaprl/theories/itt/itt_list.ml
+7 -4	metaprl/theories/itt/itt_prod.ml
+8 -4	metaprl/theories/itt/itt_quotient.ml
+10 -7	metaprl/theories/itt/itt_rfun.ml
+30 -28	metaprl/theories/itt/itt_set.ml
+5 -1	metaprl/theories/itt/itt_squash.ml
+22 -21	metaprl/theories/itt/itt_struct.ml
+7 -4	metaprl/theories/itt/itt_subtype.ml
+16 -8	metaprl/theories/itt/itt_union.ml
+6 -2	metaprl/theories/itt/itt_unit.ml
+6 -3	metaprl/theories/itt/itt_void.ml
+26 -21	metaprl/theories/tactic/options.ml
+9 -7	metaprl/theories/tactic/options.mli
+37 -46	metaprl/theories/tactic/sequent.ml
+27 -13	metaprl/theories/tactic/sequent.mli
+581 -431	metaprl/theories/tactic/tactic_cache.ml
+13 -7	metaprl/theories/tactic/tactic_cache.mli
+700 -51	metaprl/theories/tactic/tactic_type.ml
+95 -31	metaprl/theories/tactic/tactic_type.mli
+88 -179	metaprl/theories/tactic/tacticals.ml
+28 -16	metaprl/theories/tactic/tacticals.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-10 13:25:15 -0700 (Wed, 10 Jun 1998)
Revision: 2223
Log message:

Trying to make term_ds as fast as possible

Changes	Path
+26 -14	metaprl/refiner/term_ds/term_ds.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-06-12 06:47:49 -0700 (Fri, 12 Jun 1998)
Revision: 2224
Log message:

D tactic works, added itt_bool.

Changes	Path
Properties	metaprl/editor/ml
+1 -0	metaprl/editor/ml/Makefile
+1 -1	metaprl/editor/ml/nl
+84 -64	metaprl/editor/ml/package_info.ml
+7 -0	metaprl/editor/ml/package_info.mli
+6 -3	metaprl/editor/ml/proof.ml
+25 -12	metaprl/editor/ml/proof_edit.ml
+4 -1	metaprl/editor/ml/proof_step.ml
+33 -14	metaprl/editor/ml/shell.ml
+10 -0	metaprl/editor/ml/shell.mli
+5 -2	metaprl/editor/ml/shell_null.ml
+8 -0	metaprl/editor/ml/shell_p4.ml
+11 -7	metaprl/editor/ml/shell_rewrite.ml
+4 -1	metaprl/editor/ml/test.ml
+4 -0	metaprl/editor/ml/test.mli
+6 -2	metaprl/editor/ml/x.ml
+2 -1	metaprl/filter/Makefile
+139 -48	metaprl/filter/filter_cache_fun.ml
+8 -4	metaprl/filter/filter_cache_fun.mli
+4 -0	metaprl/filter/filter_exn.ml
Added	metaprl/filter/filter_grammar.ml
Properties	metaprl/filter/filter_grammar.ml
Added	metaprl/filter/filter_grammar.mli
Properties	metaprl/filter/filter_grammar.mli
+43 -83	metaprl/filter/filter_parse.ml
+30 -3	metaprl/filter/filter_prog.ml
+13 -2	metaprl/filter/filter_summary.ml
+4 -0	metaprl/filter/filter_summary.mli
+10 -1	metaprl/filter/filter_summary_type.mlz
+4 -0	metaprl/filter/filter_summary_util.ml
+9 -0	metaprl/filter/term_grammar.ml
+7 -0	metaprl/filter/term_grammar.mli
+4 -1	metaprl/library/Makefile
+197 -42	metaprl/mllib/debug.ml
+24 -46	metaprl/mllib/debug.mli
+7 -91	metaprl/mllib/debug_set.ml
+4 -7	metaprl/mllib/debug_set.mli
+9 -0	metaprl/mllib/file_base.ml
+10 -3	metaprl/mllib/list_util.ml
+93 -81	metaprl/refiner/refiner/refine.ml
+9 -0	metaprl/refiner/refiner/rewrite.ml
+0 -1	metaprl/refiner/reflib/Makefile
+70 -58	metaprl/refiner/reflib/refine_exn.ml
+15 -0	metaprl/refiner/reflib/rformat.ml
+8 -0	metaprl/refiner/reflib/rformat.mli
+9 -0	metaprl/refiner/reflib/term_table.ml
+17 -7	metaprl/refiner/refsig/refine_sig.ml
+3 -1	metaprl/refiner/refsig/term_addr_sig.ml
+5 -3	metaprl/refiner/term_gen/term_addr_gen.ml
+152 -182	metaprl/refiner/term_gen/term_man_gen.ml
+12 -5	metaprl/refiner/term_std/term_std.ml
Properties	metaprl/theories/base
+7 -5	metaprl/theories/base/base_dform.ml
+21 -3	metaprl/theories/base/base_dtactic.ml
+20 -1	metaprl/theories/base/base_rewrite.ml
+8 -0	metaprl/theories/base/base_rewrite.mli
+4 -0	metaprl/theories/base/base_theory.mlz
+4 -1	metaprl/theories/base/typeinf.ml
+1 -0	metaprl/theories/itt/Makefile
Added	metaprl/theories/itt/itt_bool.ml
Properties	metaprl/theories/itt/itt_bool.ml
Added	metaprl/theories/itt/itt_bool.mli
Properties	metaprl/theories/itt/itt_bool.mli
+7 -3	metaprl/theories/itt/itt_dfun.ml
+7 -4	metaprl/theories/itt/itt_dprod.ml
+5 -2	metaprl/theories/itt/itt_equal.ml
+5 -1	metaprl/theories/itt/itt_fun.ml
+9 -4	metaprl/theories/itt/itt_int.ml
+5 -2	metaprl/theories/itt/itt_int.mli
+5 -2	metaprl/theories/itt/itt_isect.ml
+6 -3	metaprl/theories/itt/itt_list.ml
+5 -2	metaprl/theories/itt/itt_logic.ml
+4 -1	metaprl/theories/itt/itt_prod.ml
+5 -1	metaprl/theories/itt/itt_quotient.ml
+8 -5	metaprl/theories/itt/itt_rfun.ml
+6 -3	metaprl/theories/itt/itt_set.ml
+4 -1	metaprl/theories/itt/itt_squash.ml
+8 -5	metaprl/theories/itt/itt_struct.ml
+7 -4	metaprl/theories/itt/itt_subtype.ml
+4 -0	metaprl/theories/itt/itt_theory.mlz
+10 -6	metaprl/theories/itt/itt_union.ml
+4 -1	metaprl/theories/tactic/conversionals.ml
+4 -1	metaprl/theories/tactic/tactic_cache.ml
+8 -5	metaprl/theories/tactic/tactic_type.ml
+8 -5	metaprl/theories/tactic/tacticals.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-06-12 06:55:33 -0700 (Fri, 12 Jun 1998)
Revision: 2225
Log message:

Modified resources.

Changes	Path
Added	metaprl/refiner/reflib/resource.ml
Properties	metaprl/refiner/reflib/resource.ml
Added	metaprl/refiner/reflib/resource.mli
Properties	metaprl/refiner/reflib/resource.mli
Deleted	metaprl/refiner/reflib/resource.mlz

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-06-12 11:36:50 -0700 (Fri, 12 Jun 1998)
Revision: 2226
Log message:

Working factorial proof.

Changes	Path
+26 -1	metaprl/editor/ml/test.ml
+7 -0	metaprl/editor/ml/test.mli
+7 -3	metaprl/editor/ml/x.ml
+11 -3	metaprl/filter/filter_cache_fun.ml
+3 -0	metaprl/filter/filter_summary_util.ml
+3 -1	metaprl/mllib/debug.ml
+5 -1	metaprl/mllib/list_util.ml
+9 -0	metaprl/refiner/refbase/opname.ml
+7 -0	metaprl/refiner/refbase/opname.mli
+10 -12	metaprl/refiner/reflib/dform.ml
+2 -1	metaprl/theories/itt/Makefile
+34 -2	metaprl/theories/itt/itt_bool.ml
+11 -2	metaprl/theories/itt/itt_bool.mli
+5 -3	metaprl/theories/itt/itt_int.ml
+6 -2	metaprl/theories/itt/itt_int.mli
Added	metaprl/theories/itt/itt_int_bool.ml
Properties	metaprl/theories/itt/itt_int_bool.ml
Added	metaprl/theories/itt/itt_int_bool.mli
Properties	metaprl/theories/itt/itt_int_bool.mli
+5 -0	metaprl/theories/itt/itt_rfun.ml
+4 -0	metaprl/theories/itt/itt_theory.mlz
+61 -7	metaprl/theories/tactic/conversionals.ml
+20 -0	metaprl/theories/tactic/conversionals.mli
+10 -1	metaprl/theories/tactic/tactic_type.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-06-12 13:46:09 -0700 (Fri, 12 Jun 1998)
Revision: 2227
Log message:

Switched to term_ds.

Changes	Path
+4 -1	metaprl/editor/ml/test.ml
+5 -0	metaprl/editor/ml/x.ml
+4 -1	metaprl/refiner/refiner/refiner.ml
+4 -1	metaprl/theories/tactic/conversionals.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-06-13 09:24:05 -0700 (Sat, 13 Jun 1998)
Revision: 2228
Log message:

Adding timing tactical.

Changes	Path
+8 -0	metaprl/theories/tactic/tactic_type.ml
+7 -0	metaprl/theories/tactic/tactic_type.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-13 10:27:14 -0700 (Sat, 13 Jun 1998)
Revision: 2229
Log message:

Changes	Path
+2 -2	metaprl/editor/ml/nl

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-13 11:40:21 -0700 (Sat, 13 Jun 1998)
Revision: 2230
Log message:

Added cardinal function

Changes	Path
+2 -0	metaprl/mllib/splay_set.ml
+1 -0	metaprl/mllib/splay_set.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-13 11:46:59 -0700 (Sat, 13 Jun 1998)
Revision: 2231
Log message:

Fixed a typo

Changes	Path
+1 -1	metaprl/mllib/splay_set.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-13 15:01:01 -0700 (Sat, 13 Jun 1998)
Revision: 2232
Log message:

Make it faster

Changes	Path
+1 -2	metaprl/refiner/term_ds/term_subst_ds.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-13 15:48:11 -0700 (Sat, 13 Jun 1998)
Revision: 2233
Log message:

Added rev_iter2

Changes	Path
+7 -0	metaprl/mllib/list_util.ml
+7 -1	metaprl/mllib/list_util.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-13 15:48:35 -0700 (Sat, 13 Jun 1998)
Revision: 2234
Log message:

Make it faster

Changes	Path
+4 -1	metaprl/refiner/refiner/rewrite.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-13 17:04:14 -0700 (Sat, 13 Jun 1998)
Revision: 2235
Log message:

"for_all2 f a b" should not call f when a and b have different length

Changes	Path
+4 -1	metaprl/mllib/list_util.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-13 17:58:38 -0700 (Sat, 13 Jun 1998)
Revision: 2236
Log message:

Do not define helper functions inside a function

Changes	Path
+252 -341	metaprl/mllib/list_util.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-13 18:29:37 -0700 (Sat, 13 Jun 1998)
Revision: 2237
Log message:

Make it faster

Changes	Path
+7 -14	metaprl/mllib/array_util.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-13 18:31:47 -0700 (Sat, 13 Jun 1998)
Revision: 2238
Log message:

Fixed a typo

Changes	Path
+4 -1	metaprl/mllib/array_util.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-13 18:31:48 -0700 (Sat, 13 Jun 1998)
Revision: 2239
Log message:

Make it faster

Changes	Path
+24 -26	metaprl/mllib/splay_set.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-14 14:55:54 -0700 (Sun, 14 Jun 1998)
Revision: 2240
Log message:

Speed improvements - do not create functions inside other functions

Changes	Path
+663 -712	metaprl/refiner/refiner/rewrite.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-14 15:58:52 -0700 (Sun, 14 Jun 1998)
Revision: 2241
Log message:

Make it faster

Changes	Path
+12 -25	metaprl/mllib/string_util.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-14 16:03:03 -0700 (Sun, 14 Jun 1998)
Revision: 2242
Log message:

Changes	Path
+5 -3	metaprl/mllib/imp_dag.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-06-15 14:58:07 -0700 (Mon, 15 Jun 1998)
Revision: 2243
Log message:

Added a few new functions.

Changes	Path
+4 -4	metaprl/refiner/refsig/Makefile
+7 -5	metaprl/refiner/refsig/term_man_sig.ml
+4 -1	metaprl/refiner/refsig/term_meta_sig.ml
+7 -0	metaprl/refiner/refsig/term_op_sig.ml
+7 -4	metaprl/refiner/refsig/term_simple_sig.mlz
+38 -38	metaprl/refiner/term_ds/term_ds.ml
+4 -4	metaprl/refiner/term_ds/term_ds.mli
+9 -9	metaprl/refiner/term_ds/term_eval_ds.ml
+103 -74	metaprl/refiner/term_ds/term_op_ds.ml
+28 -27	metaprl/refiner/term_ds/term_subst_ds.ml
+17 -8	metaprl/refiner/term_gen/term_addr_gen.ml
+48 -39	metaprl/refiner/term_gen/term_man_gen.ml
+11 -5	metaprl/refiner/term_gen/term_meta_gen.ml
+2 -2	metaprl/refiner/term_gen/term_shape_gen.ml
+12 -9	metaprl/refiner/term_std/term_eval_std.ml
+101 -73	metaprl/refiner/term_std/term_op_std.ml
+36 -32	metaprl/refiner/term_std/term_std.ml
+5 -2	metaprl/refiner/term_std/term_std.mli
+41 -35	metaprl/refiner/term_std/term_subst_std.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-06-15 15:33:52 -0700 (Mon, 15 Jun 1998)
Revision: 2244
Log message:

Added CZF.

Changes	Path
+1 -0	metaprl/Makefile
+4 -0	metaprl/editor/ml/Makefile
+105 -0	metaprl/editor/ml/io_proof.ml
+12 -0	metaprl/editor/ml/io_proof.mli
+1 -1	metaprl/editor/ml/nl
+144 -20	metaprl/editor/ml/package_info.ml
+7 -0	metaprl/editor/ml/package_type.mlz
+8 -3	metaprl/editor/ml/proof.ml
+4 -0	metaprl/editor/ml/proof.mli
+86 -49	metaprl/editor/ml/proof_edit.ml
+5 -2	metaprl/editor/ml/proof_edit.mli
+63 -16	metaprl/editor/ml/shell.ml
+5 -1	metaprl/editor/ml/shell.mli
+5 -1	metaprl/editor/ml/shell_null.ml
+61 -4	metaprl/editor/ml/shell_rewrite.ml
Added	metaprl/editor/ml/shell_rule.ml
Properties	metaprl/editor/ml/shell_rule.ml
Added	metaprl/editor/ml/shell_rule.mli
Properties	metaprl/editor/ml/shell_rule.mli
+5 -1	metaprl/editor/ml/shell_type.mlz
+9 -6	metaprl/editor/ml/test.ml
+32 -10	metaprl/filter/filter_bin.ml
+41 -11	metaprl/filter/filter_cache.ml
+6 -0	metaprl/filter/filter_cache.mli
+19 -0	metaprl/filter/filter_cache_fun.ml
+45 -11	metaprl/filter/filter_parse.ml
+117 -64	metaprl/filter/filter_summary.ml
+6 -2	metaprl/filter/filter_summary.mli
+8 -0	metaprl/filter/filter_summary_io.ml
+10 -0	metaprl/filter/filter_summary_type.mlz
+46 -11	metaprl/filter/prlcomp.ml
+4 -1	metaprl/filter/term_grammar.ml
+11 -10	metaprl/library/library_type_base.ml
+26 -8	metaprl/mllib/file_base.ml
+11 -6	metaprl/mllib/file_base_type.ml
+42 -25	metaprl/mllib/file_type_base.ml
+45 -4	metaprl/mllib/list_util.ml
+7 -0	metaprl/mllib/list_util.mli
+7 -2	metaprl/refiner/refbase/opname.ml
+4 -1	metaprl/refiner/refiner/refine.ml
+4 -1	metaprl/refiner/reflib/dform.ml
+53 -4	metaprl/refiner/reflib/term_table.ml
+4 -1	metaprl/refiner/reflib/term_table.mli
+5 -2	metaprl/theories/base/base_dform.ml
+20 -88	metaprl/theories/base/base_dtactic.ml
+17 -15	metaprl/theories/base/nuprl_font.ml
+6 -0	metaprl/theories/base/summary.ml
+4 -0	metaprl/theories/base/summary.mli
+4 -1	metaprl/theories/base/typeinf.ml
Properties	metaprl/theories/czf
Added	metaprl/theories/czf/czf_itt_false.ml
Properties	metaprl/theories/czf/czf_itt_false.ml
Added	metaprl/theories/czf/czf_itt_false.mli
Properties	metaprl/theories/czf/czf_itt_false.mli
Added	metaprl/theories/czf/czf_itt_set.ml
Properties	metaprl/theories/czf/czf_itt_set.ml
Added	metaprl/theories/czf/czf_itt_set.mli
Properties	metaprl/theories/czf/czf_itt_set.mli
Added	metaprl/theories/czf/czf_itt_true.ml
Properties	metaprl/theories/czf/czf_itt_true.ml
Added	metaprl/theories/czf/czf_itt_true.mli
Properties	metaprl/theories/czf/czf_itt_true.mli
Added	metaprl/theories/czf/czf_itt_wf.ml
Properties	metaprl/theories/czf/czf_itt_wf.ml
Added	metaprl/theories/czf/czf_itt_wf.mli
Properties	metaprl/theories/czf/czf_itt_wf.mli
Added	metaprl/theories/czf/czf_set.ml
Properties	metaprl/theories/czf/czf_set.ml
+4 -1	metaprl/theories/czf/czf_set.mli
Added	metaprl/theories/czf/czf_true.ml
Properties	metaprl/theories/czf/czf_true.ml
+12 -9	metaprl/theories/czf/czf_true.mli
Added	metaprl/theories/czf/czf_wf.ml
Properties	metaprl/theories/czf/czf_wf.ml
+7 -3	metaprl/theories/czf/czf_wf.mli
+1 -0	metaprl/theories/itt/Makefile
Added	metaprl/theories/itt/itt_arith.ml
Properties	metaprl/theories/itt/itt_arith.ml
Added	metaprl/theories/itt/itt_arith.mli
Properties	metaprl/theories/itt/itt_arith.mli
+10 -7	metaprl/theories/itt/itt_bool.ml
+10 -7	metaprl/theories/itt/itt_bool.mli
+4 -1	metaprl/theories/itt/itt_dprod.ml
+4 -1	metaprl/theories/itt/itt_dprod.mli
+13 -1	metaprl/theories/itt/itt_equal.ml
+4 -1	metaprl/theories/itt/itt_ext_equal.ml
+4 -1	metaprl/theories/itt/itt_ext_equal.mli
+64 -19	metaprl/theories/itt/itt_int.ml
+51 -14	metaprl/theories/itt/itt_int.mli
+5 -2	metaprl/theories/itt/itt_list.ml
+5 -2	metaprl/theories/itt/itt_list.mli
+23 -16	metaprl/theories/itt/itt_logic.ml
+14 -8	metaprl/theories/itt/itt_logic.mli
+4 -1	metaprl/theories/itt/itt_prec.ml
+4 -1	metaprl/theories/itt/itt_prec.mli
+5 -2	metaprl/theories/itt/itt_rfun.ml
+5 -2	metaprl/theories/itt/itt_rfun.mli
+9 -5	metaprl/theories/itt/itt_squash.ml
+4 -1	metaprl/theories/itt/itt_srec.ml
+4 -1	metaprl/theories/itt/itt_srec.mli
+4 -0	metaprl/theories/itt/itt_theory.mlz
+5 -2	metaprl/theories/itt/itt_union.ml
+5 -2	metaprl/theories/itt/itt_union.mli
+4 -0	metaprl/theories/itt/itt_void.ml
+4 -0	metaprl/theories/itt/itt_void.mli
+9 -4	metaprl/theories/tactic/conversionals.ml
+4 -0	metaprl/theories/tactic/conversionals.mli
+4 -1	metaprl/theories/tactic/sequent.ml
+43 -2	metaprl/theories/tactic/tactic_type.ml
+4 -0	metaprl/theories/tactic/tactic_type.mli
+6 -1	metaprl/theories/tactic/tacticals.ml
+5 -0	metaprl/theories/tactic/tacticals.mli
+43 -0	metaprl/theories/tactic/var.ml
+9 -0	metaprl/theories/tactic/var.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-06-15 15:41:33 -0700 (Mon, 15 Jun 1998)
Revision: 2245
Log message:

Added Makefile.

Changes	Path
Added	metaprl/theories/czf/Makefile
Properties	metaprl/theories/czf/Makefile

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-15 15:53:56 -0700 (Mon, 15 Jun 1998)
Revision: 2246
Log message:

Use == for comparing opnames

Changes	Path
+1 -1	metaprl/refiner/term_ds/term_ds.ml
+2 -2	metaprl/refiner/term_ds/term_subst_ds.ml
+4 -1	metaprl/refiner/term_std/term_std.ml
+6 -3	metaprl/refiner/term_std/term_subst_std.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-15 15:57:57 -0700 (Mon, 15 Jun 1998)
Revision: 2247
Log message:

Changes	Path
+9 -10	metaprl/mllib/list_util.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-15 20:35:32 -0700 (Mon, 15 Jun 1998)
Revision: 2248
Log message:

Added OCAMLCP variable - if set to ocamlcp, make produces profiled code

Changes	Path
+4 -1	metaprl/mk/config

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-16 00:33:35 -0700 (Tue, 16 Jun 1998)
Revision: 2249
Log message:

"make profile" seems to be working

Changes	Path
+11 -4	metaprl/Makefile
+2 -2	metaprl/mk/config

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-16 09:14:13 -0700 (Tue, 16 Jun 1998)
Revision: 2250
Log message:

Added set_writable ()

Changes	Path
+4 -0	metaprl/editor/ml/x.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-06-16 09:26:27 -0700 (Tue, 16 Jun 1998)
Revision: 2251
Log message:

Added itt_test.

Changes	Path
+5 -1	metaprl/Makefile
+5 -1	metaprl/editor/ml/package_info.ml
+42 -18	metaprl/editor/ml/proof_edit.ml
+7 -4	metaprl/editor/ml/shell_p4.ml
+6 -2	metaprl/filter/Makefile
+5 -2	metaprl/filter/buffer.ml
+10 -6	metaprl/filter/filter_cache.ml
+22 -3	metaprl/filter/filter_prog.ml
+35 -20	metaprl/filter/prlcomp.ml
+7 -4	metaprl/horus/util.ml
+4 -7	metaprl/library/ascii_scan.ml
+7 -7	metaprl/library/db.ml
+10 -24	metaprl/library/mathBus.ml
+8 -5	metaprl/library/registry.ml
+2 -2	metaprl/mk/config
+4 -1	metaprl/mllib/file_util.ml
+7 -4	metaprl/mllib/filename_util.ml
+59 -1	metaprl/mllib/string_util.ml
+12 -0	metaprl/mllib/string_util.mli
+1 -1	metaprl/refiner/Makefile
+5 -2	metaprl/refiner/reflib/ml_string.ml
+7 -4	metaprl/refiner/reflib/rformat.ml
+20 -15	metaprl/refiner/reflib/term_table.ml
+7 -0	metaprl/refiner/reflib/term_table.mli
+2 -1	metaprl/theories/czf/Makefile
+39 -1	metaprl/theories/czf/czf_itt_false.ml
+3 -1	metaprl/theories/czf/czf_itt_false.mli
Added	metaprl/theories/czf/czf_itt_or.ml
Properties	metaprl/theories/czf/czf_itt_or.ml
Added	metaprl/theories/czf/czf_itt_or.mli
Properties	metaprl/theories/czf/czf_itt_or.mli
+7 -1	metaprl/theories/czf/czf_itt_set.ml
+7 -1	metaprl/theories/czf/czf_itt_set.mli
+40 -0	metaprl/theories/czf/czf_itt_true.ml
+46 -1	metaprl/theories/itt/Makefile
Added	metaprl/theories/itt/itt_test.ml
Properties	metaprl/theories/itt/itt_test.ml
Added	metaprl/theories/itt/itt_test.mli
Properties	metaprl/theories/itt/itt_test.mli
+18 -0	metaprl/theories/itt/itt_union.ml
+8 -0	metaprl/theories/itt/itt_union.mli
Added	metaprl/theories/itt/test.ml
Properties	metaprl/theories/itt/test.ml
+20 -12	metaprl/theories/itt/test.mli
+1 -0	metaprl/theories/ocaml/Makefile
+4 -0	metaprl/theories/tactic/sequent.ml
+4 -0	metaprl/theories/tactic/sequent.mli
+40 -3	metaprl/theories/tactic/tactic_type.ml
+4 -0	metaprl/theories/tactic/tactic_type.mli
+4 -1	metaprl/theories/tactic/var.ml
+2 -1	metaprl/util/Makefile

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-06-16 09:28:20 -0700 (Tue, 16 Jun 1998)
Revision: 2252
Log message:

Added magic numbers.

Changes	Path
Added	metaprl/filter/filter_magic.ml
Properties	metaprl/filter/filter_magic.ml
Added	metaprl/filter/filter_magic.mli
Properties	metaprl/filter/filter_magic.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-16 10:35:35 -0700 (Tue, 16 Jun 1998)
Revision: 2253
Log message:

Do not create functions inside a function

Changes	Path
+51 -57	metaprl/refiner/term_ds/term_subst_ds.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-16 11:14:39 -0700 (Tue, 16 Jun 1998)
Revision: 2254
Log message:

Use CAMLPLIB environment variable

Changes	Path
+1 -1	metaprl/editor/ml/nl

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-16 11:33:58 -0700 (Tue, 16 Jun 1998)
Revision: 2255
Log message:

Profiling

Changes	Path
Properties	metaprl/editor/ml
Properties	metaprl/theories/itt
+1 -1	metaprl/theories/itt/Makefile

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-06-17 06:18:33 -0700 (Wed, 17 Jun 1998)
Revision: 2256
Log message:

Added ml_term.

Changes	Path
+1 -0	metaprl/refiner/reflib/Files
Added	metaprl/refiner/reflib/ml_term.ml
Properties	metaprl/refiner/reflib/ml_term.ml
Added	metaprl/refiner/reflib/ml_term.mli
Properties	metaprl/refiner/reflib/ml_term.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-06-17 06:19:43 -0700 (Wed, 17 Jun 1998)
Revision: 2257
Log message:

Using marshaler for terms.

Changes	Path
+36 -26	metaprl/filter/filter_prog.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-06-17 08:46:02 -0700 (Wed, 17 Jun 1998)
Revision: 2258
Log message:

Optimizing compiler.

Changes	Path
+4 -10	metaprl/clib/Makefile
Deleted	metaprl/clib/punix.ml
Deleted	metaprl/clib/punix.mli
+0 -2	metaprl/editor/ml/Makefile
Deleted	metaprl/editor/ml/make1
+0 -3	metaprl/filter/Makefile
+1 -1	metaprl/library/Makefile
+11 -8	metaprl/mk/config
+2 -1	metaprl/mllib/Makefile
+55 -36	metaprl/mllib/string_util.ml
+1 -1	metaprl/refiner/Makefile
+9 -2	metaprl/refiner/reflib/ml_term.ml
+2 -4	metaprl/theories/itt/Makefile
+16 -3	metaprl/theories/itt/itt_test.ml
Added	metaprl/theories/itt/test
Properties	metaprl/theories/itt/test

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-06-17 09:59:01 -0700 (Wed, 17 Jun 1998)
Revision: 2259
Log message:

Added punix.ml

Changes	Path
Added	metaprl/mllib/punix.ml
Properties	metaprl/mllib/punix.ml
Added	metaprl/mllib/punix.mli
Properties	metaprl/mllib/punix.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-06-17 12:38:58 -0700 (Wed, 17 Jun 1998)
Revision: 2260
Log message:

Did some profiling.

Changes	Path
+8 -8	metaprl/filter/Makefile
+4 -3	metaprl/mk/config
+11 -0	metaprl/refiner/refiner/rewrite.ml
+1 -1	metaprl/theories/itt/Makefile

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-17 12:51:24 -0700 (Wed, 17 Jun 1998)
Revision: 2261
Log message:

Changes	Path
Properties	metaprl/refiner
Properties	metaprl/theories/itt

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-17 22:25:25 -0700 (Wed, 17 Jun 1998)
Revision: 2262
Log message:

      Added a dependency, so that make does not try
      to build refiner.cm[x]a before */reflib.cm[x]a

Changes	Path
+2 -1	metaprl/refiner/Makefile

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-19 18:31:38 -0700 (Fri, 19 Jun 1998)
Revision: 2263
Log message:

Added a dependecy for native code build

Changes	Path
+1 -0	metaprl/refiner/Makefile

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-19 18:31:59 -0700 (Fri, 19 Jun 1998)
Revision: 2264
Log message:

Removed all runtime closure creations

Changes	Path
+132 -148	metaprl/refiner/term_gen/term_addr_gen.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-19 18:34:50 -0700 (Fri, 19 Jun 1998)
Revision: 2265
Log message:

OCAMLCPOPT allows to pass options to bytecode profiler

Changes	Path
+8 -5	metaprl/Makefile
+3 -2	metaprl/mk/config

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-19 18:56:06 -0700 (Fri, 19 Jun 1998)
Revision: 2266
Log message:

Changes	Path
Properties	metaprl/theories/itt

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-19 22:38:56 -0700 (Fri, 19 Jun 1998)
Revision: 2267
Log message:

Fixed some typos

Changes	Path
+3 -3	metaprl/refiner/term_gen/term_addr_gen.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-06-22 12:46:48 -0700 (Mon, 22 Jun 1998)
Revision: 2268
Log message:

      Rewriting in contexts.  This required a change in addressing,
      and the body of the context is the _last_ subterm, not the first.

Changes	Path
+1 -1	metaprl/Makefile
Properties	metaprl/editor/ml
Added	metaprl/editor/ml/y.ml
Properties	metaprl/editor/ml/y.ml
Properties	metaprl/filter
+25 -5	metaprl/filter/filter_bin.ml
+28 -6	metaprl/filter/filter_cache_fun.ml
+6 -0	metaprl/filter/filter_parse.ml
+5 -1	metaprl/filter/filter_summary_io.ml
Properties	metaprl/library
Properties	metaprl/mllib
+20 -0	metaprl/mllib/array_util.ml
+6 -0	metaprl/mllib/array_util.mli
+14 -6	metaprl/mllib/debug.ml
+7 -1	metaprl/mllib/debug.mli
+27 -0	metaprl/mllib/list_util.ml
+8 -1	metaprl/mllib/list_util.mli
Properties	metaprl/refiner
+5 -2	metaprl/refiner/Makefile
Properties	metaprl/refiner/refbase
+21 -0	metaprl/refiner/refbase/opname.ml
+5 -0	metaprl/refiner/refbase/opname.mli
Properties	metaprl/refiner/refiner
+19 -0	metaprl/refiner/refiner/refine.ml
+313 -32	metaprl/refiner/refiner/rewrite.ml
Properties	metaprl/refiner/reflib
+8 -0	metaprl/refiner/reflib/simple_print.ml
Properties	metaprl/refiner/refsig
+4 -1	metaprl/refiner/refsig/refine_sig.ml
+11 -1	metaprl/refiner/refsig/term_addr_sig.ml
+8 -0	metaprl/refiner/refsig/term_simple_sig.mlz
Properties	metaprl/refiner/term_ds
+45 -14	metaprl/refiner/term_ds/term_ds.ml
+5 -0	metaprl/refiner/term_ds/term_ds.mli
+80 -23	metaprl/refiner/term_ds/term_subst_ds.ml
Properties	metaprl/refiner/term_gen
+61 -40	metaprl/refiner/term_gen/term_addr_gen.ml
+47 -16	metaprl/refiner/term_gen/term_man_gen.ml
Properties	metaprl/refiner/term_std
+30 -9	metaprl/refiner/term_std/term_std.ml
+9 -0	metaprl/refiner/term_std/term_std.mli
+28 -15	metaprl/refiner/term_std/term_subst_std.ml
Properties	metaprl/theories/base
+23 -0	metaprl/theories/base/base_dform.ml
+9 -6	metaprl/theories/base/base_rewrite.ml
+10 -4	metaprl/theories/base/base_rewrite.mli
Properties	metaprl/theories/czf
+10 -5	metaprl/theories/czf/czf_itt_or.ml
+5 -1	metaprl/theories/czf/czf_itt_or.mli
+29 -5	metaprl/theories/czf/czf_itt_wf.ml
+15 -3	metaprl/theories/czf/czf_itt_wf.mli
+0 -3	metaprl/theories/itt/Makefile
+6 -2	metaprl/theories/itt/itt_atom.ml
+11 -7	metaprl/theories/itt/itt_dprod.ml
+6 -2	metaprl/theories/itt/itt_dprod.mli
+18 -2	metaprl/theories/itt/itt_equal.ml
+16 -0	metaprl/theories/itt/itt_equal.mli
+6 -1	metaprl/theories/itt/itt_list.ml
+8 -0	metaprl/theories/itt/itt_list.mli
+8 -0	metaprl/theories/itt/itt_logic.ml
+7 -2	metaprl/theories/itt/itt_quotient.ml
+8 -0	metaprl/theories/itt/itt_quotient.mli
+5 -0	metaprl/theories/itt/itt_rfun.ml
+5 -1	metaprl/theories/itt/itt_struct.ml
+7 -1	metaprl/theories/itt/itt_subtype.ml
+8 -0	metaprl/theories/itt/itt_subtype.mli
Deleted	metaprl/theories/itt/itt_theory.mlz
+7 -3	metaprl/theories/itt/itt_union.ml
+6 -2	metaprl/theories/itt/itt_union.mli
Properties	metaprl/theories/ocaml
+1 -2	metaprl/theories/ocaml/Makefile
Deleted	metaprl/theories/ocaml/perv.ml
Deleted	metaprl/theories/ocaml/perv.mli
Properties	metaprl/theories/ocaml_sos
Properties	metaprl/theories/rewrite
Properties	metaprl/theories/tactic
+4 -3	metaprl/theories/tactic/Makefile
+17 -0	metaprl/theories/tactic/conversionals.ml
+6 -0	metaprl/theories/tactic/conversionals.mli
Added	metaprl/theories/tactic/perv.ml
Properties	metaprl/theories/tactic/perv.ml
Added	metaprl/theories/tactic/perv.mli
Properties	metaprl/theories/tactic/perv.mli
+163 -18	metaprl/theories/tactic/rewrite_type.ml
+44 -0	metaprl/theories/tactic/rewrite_type.mli
+21 -2	metaprl/theories/tactic/tactic_type.ml
+6 -0	metaprl/theories/tactic/tacticals.ml
+5 -0	metaprl/theories/tactic/tacticals.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-06-22 13:01:44 -0700 (Mon, 22 Jun 1998)
Revision: 2269
Log message:

Fixed syntax error in term_addr_gen.ml

Changes	Path
+4 -4	metaprl/refiner/term_gen/term_addr_gen.ml
+6 -3	metaprl/theories/czf/czf_itt_or.ml
+4 -1	metaprl/theories/tactic/rewrite_type.ml
+4 -1	metaprl/theories/tactic/rewrite_type.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-22 14:41:47 -0700 (Mon, 22 Jun 1998)
Revision: 2270
Log message:

Better profiling

Changes	Path
+3 -4	metaprl/Makefile

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-23 01:16:21 -0700 (Tue, 23 Jun 1998)
Revision: 2271
Log message:

Compile ocamldep to native code

Changes	Path
+8 -7	metaprl/util/Makefile

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-06-23 15:12:44 -0700 (Tue, 23 Jun 1998)
Revision: 2272
Log message:

Improved rewriter speed with conversion tree and flist.

Changes	Path
+5 -2	metaprl/editor/ml/shell_rule.ml
+15 -2	metaprl/editor/ml/y.ml
+5 -3	metaprl/filter/filter_prog.ml
+2 -1	metaprl/mllib/Makefile
Added	metaprl/mllib/flist.ml
Properties	metaprl/mllib/flist.ml
Added	metaprl/mllib/flist.mli
Properties	metaprl/mllib/flist.mli
+7 -0	metaprl/refiner/refiner/refine.ml
+73 -26	metaprl/refiner/refiner/rewrite.ml
+13 -1	metaprl/refiner/term_ds/term_subst_ds.ml
Properties	metaprl/theories/czf
+8 -1	metaprl/theories/czf/Makefile
Added	metaprl/theories/czf/czf_itt_all.ml
Properties	metaprl/theories/czf/czf_itt_all.ml
Added	metaprl/theories/czf/czf_itt_all.mli
Properties	metaprl/theories/czf/czf_itt_all.mli
Added	metaprl/theories/czf/czf_itt_and.ml
Properties	metaprl/theories/czf/czf_itt_and.ml
Added	metaprl/theories/czf/czf_itt_and.mli
Properties	metaprl/theories/czf/czf_itt_and.mli
Added	metaprl/theories/czf/czf_itt_axioms.ml
Properties	metaprl/theories/czf/czf_itt_axioms.ml
Added	metaprl/theories/czf/czf_itt_axioms.mli
Properties	metaprl/theories/czf/czf_itt_axioms.mli
Added	metaprl/theories/czf/czf_itt_dall.ml
Properties	metaprl/theories/czf/czf_itt_dall.ml
Added	metaprl/theories/czf/czf_itt_dall.mli
Properties	metaprl/theories/czf/czf_itt_dall.mli
Added	metaprl/theories/czf/czf_itt_dexists.ml
Properties	metaprl/theories/czf/czf_itt_dexists.ml
Added	metaprl/theories/czf/czf_itt_dexists.mli
Properties	metaprl/theories/czf/czf_itt_dexists.mli
Added	metaprl/theories/czf/czf_itt_exists.ml
Properties	metaprl/theories/czf/czf_itt_exists.ml
Added	metaprl/theories/czf/czf_itt_exists.mli
Properties	metaprl/theories/czf/czf_itt_exists.mli
Added	metaprl/theories/czf/czf_itt_implies.ml
Properties	metaprl/theories/czf/czf_itt_implies.ml
Added	metaprl/theories/czf/czf_itt_implies.mli
Properties	metaprl/theories/czf/czf_itt_implies.mli
+7 -0	metaprl/theories/czf/czf_itt_or.ml
+7 -0	metaprl/theories/czf/czf_itt_or.mli
+73 -6	metaprl/theories/czf/czf_itt_set.ml
+47 -6	metaprl/theories/czf/czf_itt_set.mli
+2 -2	metaprl/theories/itt/Makefile
+7 -4	metaprl/theories/itt/itt_dfun.ml
+6 -3	metaprl/theories/itt/itt_dfun.mli
+13 -14	metaprl/theories/itt/itt_dprod.ml
+5 -2	metaprl/theories/itt/itt_dprod.mli
+4 -1	metaprl/theories/itt/itt_fun.ml
+11 -8	metaprl/theories/itt/itt_logic.ml
+6 -6	metaprl/theories/itt/itt_prod.ml
+5 -2	metaprl/theories/itt/itt_rfun.ml
+8 -5	metaprl/theories/itt/itt_struct.ml
+4 -2	metaprl/theories/itt/itt_test.ml
+73 -44	metaprl/theories/tactic/conversionals.ml
+5 -0	metaprl/theories/tactic/conversionals.mli
+148 -35	metaprl/theories/tactic/rewrite_type.ml
+12 -2	metaprl/theories/tactic/rewrite_type.mli
+74 -97	metaprl/theories/tactic/tactic_type.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-23 19:24:21 -0700 (Tue, 23 Jun 1998)
Revision: 2273
Log message:

Changes	Path
+9 -10	metaprl/refiner/term_gen/term_addr_gen.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-24 23:32:23 -0700 (Wed, 24 Jun 1998)
Revision: 2274
Log message:

Do not pass $(PROFILE) flag to $(OCAMLC)

Changes	Path
+2 -2	metaprl/mk/config

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-26 19:21:40 -0700 (Fri, 26 Jun 1998)
Revision: 2275
Log message:

Changes	Path
+4 -1	metaprl/refiner/refiner/rewrite.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-26 19:25:06 -0700 (Fri, 26 Jun 1998)
Revision: 2276
Log message:

Added -compact option

Changes	Path
+4 -0	metaprl/filter/prlcomp.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-26 19:34:19 -0700 (Fri, 26 Jun 1998)
Revision: 2277
Log message:

Added a dependency

Changes	Path
+1 -1	metaprl/refiner/Makefile

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-26 22:25:30 -0700 (Fri, 26 Jun 1998)
Revision: 2278
Log message:

Changes	Path
+2 -1	metaprl/refiner/Makefile

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-26 22:29:50 -0700 (Fri, 26 Jun 1998)
Revision: 2279
Log message:

Prevent some closure creations

Changes	Path
+54 -52	metaprl/theories/tactic/rewrite_type.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-30 21:38:04 -0700 (Tue, 30 Jun 1998)
Revision: 2280
Log message:

Moved Refiner exceptions into a separate module RefineErrors

Changes	Path
+4 -0	metaprl/editor/ml/proof.ml
+4 -1	metaprl/editor/ml/proof.mli
+4 -0	metaprl/editor/ml/proof_edit.ml
+5 -1	metaprl/editor/ml/proof_step.ml
+4 -1	metaprl/editor/ml/shell.ml
+4 -1	metaprl/editor/ml/shell_null.ml
+4 -0	metaprl/editor/ml/shell_rewrite.ml
+4 -0	metaprl/editor/ml/shell_rule.ml
+1 -0	metaprl/refiner/refiner/Files
+17 -38	metaprl/refiner/refiner/refine.ml
+9 -2	metaprl/refiner/refiner/refine.mli
Added	metaprl/refiner/refiner/refine_errors.ml
Properties	metaprl/refiner/refiner/refine_errors.ml
Added	metaprl/refiner/refiner/refine_errors.mli
Properties	metaprl/refiner/refiner/refine_errors.mli
+6 -2	metaprl/refiner/refiner/refiner_ds.ml
+6 -2	metaprl/refiner/refiner/refiner_std.ml
+85 -105	metaprl/refiner/refiner/rewrite.ml
+12 -3	metaprl/refiner/refiner/rewrite.mli
+6 -3	metaprl/refiner/reflib/refine_exn.ml
+4 -2	metaprl/refiner/reflib/refine_exn.mli
Properties	metaprl/refiner/refsig
+1 -0	metaprl/refiner/refsig/Files
Added	metaprl/refiner/refsig/refine_errors_sig.mlz
Properties	metaprl/refiner/refsig/refine_errors_sig.mlz
+3 -30	metaprl/refiner/refsig/refine_sig.ml
+10 -3	metaprl/refiner/refsig/refiner_sig.ml
+3 -22	metaprl/refiner/refsig/rewrite_sig.ml
+4 -1	metaprl/theories/base/base_dtactic.ml
+4 -1	metaprl/theories/base/base_rewrite.ml
+4 -1	metaprl/theories/base/typeinf.ml
+4 -1	metaprl/theories/czf/czf_itt_all.ml
+4 -1	metaprl/theories/czf/czf_itt_and.ml
+4 -1	metaprl/theories/czf/czf_itt_dall.ml
+4 -1	metaprl/theories/czf/czf_itt_dexists.ml
+4 -1	metaprl/theories/czf/czf_itt_exists.ml
+4 -1	metaprl/theories/czf/czf_itt_false.ml
+4 -1	metaprl/theories/czf/czf_itt_implies.ml
+4 -1	metaprl/theories/czf/czf_itt_or.ml
+4 -1	metaprl/theories/czf/czf_itt_set.ml
+4 -1	metaprl/theories/czf/czf_itt_true.ml
+4 -1	metaprl/theories/czf/czf_itt_wf.ml
+4 -1	metaprl/theories/itt/itt_arith.ml
+4 -1	metaprl/theories/itt/itt_dfun.ml
+4 -1	metaprl/theories/itt/itt_dprod.ml
+7 -4	metaprl/theories/itt/itt_equal.ml
+4 -1	metaprl/theories/itt/itt_fun.ml
+4 -1	metaprl/theories/itt/itt_int.ml
+4 -1	metaprl/theories/itt/itt_isect.ml
+6 -2	metaprl/theories/itt/itt_list.ml
+4 -1	metaprl/theories/itt/itt_logic.ml
+4 -1	metaprl/theories/itt/itt_prod.ml
+4 -1	metaprl/theories/itt/itt_quotient.ml
+4 -1	metaprl/theories/itt/itt_rfun.ml
+4 -1	metaprl/theories/itt/itt_set.ml
+4 -1	metaprl/theories/itt/itt_squash.ml
+4 -1	metaprl/theories/itt/itt_struct.ml
+4 -1	metaprl/theories/itt/itt_subtype.ml
+5 -2	metaprl/theories/itt/itt_union.ml
+4 -1	metaprl/theories/tactic/conversionals.ml
+4 -1	metaprl/theories/tactic/conversionals.mli
+5 -1	metaprl/theories/tactic/rewrite_type.ml
+4 -0	metaprl/theories/tactic/tactic_cache.ml
+4 -0	metaprl/theories/tactic/tactic_type.ml
+4 -1	metaprl/theories/tactic/tacticals.ml