Commit log for MetaPRL

Changes by: Richard Eaton (eaton at cs.cornell.edu)
Date: 1998-04-03 10:07:35 -0800 (Fri, 03 Apr 1998)
Revision: 2100
Log message:

Changes	Path
+1 -1	metaprl/library/Makefile
+20 -1	metaprl/library/definition.ml
+2 -1	metaprl/library/library.ml
+1 -1	metaprl/library/library.mli
+57 -5	metaprl/library/library_type_base.ml
+6 -2	metaprl/library/library_type_base.mli
+3 -2	metaprl/library/orb.ml
+12 -5	metaprl/library/test.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-06 12:50:41 -0700 (Mon, 06 Apr 1998)
Revision: 2101
Log message:

Fixed match error in mLast_util.ml

Changes	Path
+19 -1	metaprl/filter/filter_comment.ml
+55 -19	metaprl/filter/mLast_util.ml
+15 -10	metaprl/filter/mLast_util.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-06 14:31:17 -0700 (Mon, 06 Apr 1998)
Revision: 2102
Log message:

Items must be reversed.

Changes	Path
+4 -1	metaprl/filter/filter_summary.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-06 14:39:55 -0700 (Mon, 06 Apr 1998)
Revision: 2103
Log message:

Test program with a sequent.

Changes	Path
+4 -3	metaprl/filter/test.ml
+5 -1	metaprl/filter/test.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-06 15:00:47 -0700 (Mon, 06 Apr 1998)
Revision: 2104
Log message:

Added nums library.

Changes	Path
+2 -7	metaprl/library/Makefile

Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 1998-04-07 11:08:03 -0700 (Tue, 07 Apr 1998)
Revision: 2105
Log message:

mathbus, num, int32

Changes	Path
+5 -2	metaprl/library/Makefile
+7 -7	metaprl/library/basic.ml
+2 -2	metaprl/library/basic.mli
Added	metaprl/library/int32.ml
Properties	metaprl/library/int32.ml
Added	metaprl/library/int32.mli
Properties	metaprl/library/int32.mli
+142 -89	metaprl/library/mathBus.ml
+28 -24	metaprl/library/mathBus.mli
+73 -127	metaprl/library/mbterm.ml
+1 -1	metaprl/library/mbterm.mli
+3 -3	metaprl/library/nuprl5.ml
+3 -3	metaprl/library/nuprl5.mli
+0 -0	metaprl/library/orb.ml
+50 -66	metaprl/library/registry.ml
+10 -14	metaprl/library/registry.mli
Added	metaprl/library/registry.txt
Properties	metaprl/library/registry.txt
+1 -1	metaprl/library/test.ml

Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 1998-04-07 11:15:07 -0700 (Tue, 07 Apr 1998)
Revision: 2106
Log message:

Changes	Path
+1 -1	metaprl/library/registry.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-08 07:57:37 -0700 (Wed, 08 Apr 1998)
Revision: 2107
Log message:

ImpDag is in mllib.

Changes	Path
+4 -13	metaprl/editor/ml/Makefile
Deleted	metaprl/editor/ml/file_util.ml
Deleted	metaprl/editor/ml/file_util.mli
Deleted	metaprl/editor/ml/imp_dag.ml
Deleted	metaprl/editor/ml/imp_dag.mli
+3 -1	metaprl/filter/filter_cache.ml
+4 -1	metaprl/filter/filter_debug.ml
+5 -2	metaprl/mllib/Makefile
Added	metaprl/mllib/bitset.ml
Properties	metaprl/mllib/bitset.ml
Added	metaprl/mllib/bitset.mli
Properties	metaprl/mllib/bitset.mli
Added	metaprl/mllib/dag.mlz
Properties	metaprl/mllib/dag.mlz
+63 -0	metaprl/mllib/file_util.ml
+10 -0	metaprl/mllib/file_util.mli
Added	metaprl/mllib/imp_dag.ml
Properties	metaprl/mllib/imp_dag.ml
Added	metaprl/mllib/imp_dag.mli
Properties	metaprl/mllib/imp_dag.mli
Added	metaprl/mllib/precedence.ml
Properties	metaprl/mllib/precedence.ml
Added	metaprl/mllib/precedence.mli
Properties	metaprl/mllib/precedence.mli
+55 -248	metaprl/refiner/precedence.ml
+26 -24	metaprl/refiner/precedence.mli
Added	metaprl/refiner/refiner_exn.ml
Properties	metaprl/refiner/refiner_exn.ml
Added	metaprl/refiner/refiner_exn.mli
Properties	metaprl/refiner/refiner_exn.mli
+7 -4	metaprl/theories/tactic/tactic_cache.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-08 08:08:37 -0700 (Wed, 08 Apr 1998)
Revision: 2108
Log message:

Moved precedence to mllib.

Changes	Path
+1 -0	metaprl/mllib/Makefile
+59 -262	metaprl/mllib/precedence.ml
+40 -37	metaprl/mllib/precedence.mli
+0 -1	metaprl/refiner/Makefile
Deleted	metaprl/refiner/precedence.ml
Deleted	metaprl/refiner/precedence.mli
+4 -1	metaprl/theories/tactic/tactic_cache.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-08 08:16:36 -0700 (Wed, 08 Apr 1998)
Revision: 2109
Log message:

Added print for debugging.

Changes	Path
+1 -1	metaprl/library/Makefile
+7 -7	metaprl/library/registry.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-08 08:58:26 -0700 (Wed, 08 Apr 1998)
Revision: 2110
Log message:

      Updated registry.ml to fix read_string,
      and adjust the style.

Changes	Path
+147 -86	metaprl/library/registry.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-08 09:00:35 -0700 (Wed, 08 Apr 1998)
Revision: 2111
Log message:

Use standard ocamldep.

Changes	Path
+1 -1	metaprl/mk/config

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-08 10:56:48 -0700 (Wed, 08 Apr 1998)
Revision: 2112
Log message:

Add a sequent.

Changes	Path
+5 -2	metaprl/filter/test.mli

Changes by: Richard Eaton (eaton at cs.cornell.edu)
Date: 1998-04-08 11:10:36 -0700 (Wed, 08 Apr 1998)
Revision: 2113
Log message:

Changes	Path
+4 -0	metaprl/library/basic.ml
+33 -0	metaprl/library/library.ml
+5 -0	metaprl/library/library.mli
+4 -1	metaprl/library/library_type_base.ml
+37 -9	metaprl/library/orb.ml
+1 -1	metaprl/library/test.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-08 13:47:25 -0700 (Wed, 08 Apr 1998)
Revision: 2114
Log message:

Errnoneous label.

Changes	Path
+4 -1	metaprl/filter/filter_debug.ml
+5 -1	metaprl/filter/test.ml

Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 1998-04-08 13:51:37 -0700 (Wed, 08 Apr 1998)
Revision: 2115
Log message:

reg file

Changes	Path
+4 -1	metaprl/library/registry.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-09 08:26:48 -0700 (Thu, 09 Apr 1998)
Revision: 2116
Log message:

Added strip_mfunction.

Changes	Path
+18 -4	metaprl/filter/filter_parse.ml
+1 -0	metaprl/refiner/Makefile
Added	metaprl/refiner/refine_exn.ml
Properties	metaprl/refiner/refine_exn.ml
Added	metaprl/refiner/refine_exn.mli
Properties	metaprl/refiner/refine_exn.mli
Deleted	metaprl/refiner/refiner_exn.ml
Deleted	metaprl/refiner/refiner_exn.mli
+12 -0	metaprl/refiner/term_util.ml
+4 -0	metaprl/refiner/term_util.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-09 11:26:13 -0700 (Thu, 09 Apr 1998)
Revision: 2117
Log message:

Working compiler once again.

Changes	Path
+4 -4	metaprl/filter/Makefile
+4 -2	metaprl/filter/filter_ast.ml
+8 -2	metaprl/filter/filter_bin.ml
+18 -2	metaprl/filter/filter_cache.ml
+8 -5	metaprl/filter/filter_cache_fun.ml
+19 -11	metaprl/filter/filter_parse.ml
+40 -5	metaprl/filter/filter_prog.ml
+10 -4	metaprl/filter/filter_prog.mli
+15 -11	metaprl/filter/filter_summary.ml
+5 -2	metaprl/library/registry.ml
Properties	metaprl/mllib
+14 -10	metaprl/refiner/simple_print.ml
+8 -2	metaprl/refiner/term_util.ml
+4 -0	metaprl/theories/itt/itt_dprod.ml
+7 -6	metaprl/theories/itt/itt_equal.ml
+4 -0	metaprl/theories/itt/itt_fun.ml
+4 -0	metaprl/theories/itt/itt_int.ml
+5 -2	metaprl/theories/itt/itt_int.mli
+4 -0	metaprl/theories/itt/itt_isect.ml
+4 -0	metaprl/theories/itt/itt_list.ml
+4 -0	metaprl/theories/itt/itt_prod.ml
+4 -0	metaprl/theories/itt/itt_quotient.ml
+2 -0	metaprl/theories/itt/itt_redrules.ml
+4 -0	metaprl/theories/itt/itt_rfun.ml
+5 -2	metaprl/theories/itt/itt_set.mli
+4 -0	metaprl/theories/itt/itt_union.ml
+4 -0	metaprl/theories/itt/itt_unit.ml
+4 -0	metaprl/theories/itt/itt_void.ml
+3 -0	metaprl/theories/itt/itt_void.mli
+4 -1	metaprl/theories/tactic/tacticals.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-09 11:35:27 -0700 (Thu, 09 Apr 1998)
Revision: 2118
Log message:

Changed edit_type to edit_type.mlz

Changes	Path
Deleted	metaprl/editor/ml/edit_type.ml
Deleted	metaprl/editor/ml/edit_type.mli
Added	metaprl/editor/ml/edit_type.mlz
Properties	metaprl/editor/ml/edit_type.mlz

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-09 12:07:29 -0700 (Thu, 09 Apr 1998)
Revision: 2119
Log message:

Updating the editor.

Changes	Path
+1 -2	metaprl/editor/ml/Makefile
+23 -26	metaprl/editor/ml/package_info.mli
+4 -1	metaprl/editor/ml/proof.ml
+6 -3	metaprl/editor/ml/proof.mli
+4 -1	metaprl/editor/ml/proof_edit.mli
+5 -2	metaprl/editor/ml/proof_step.ml
+6 -3	metaprl/editor/ml/proof_step.mli

Changes by: Richard Eaton (eaton at cs.cornell.edu)
Date: 1998-04-09 13:19:37 -0700 (Thu, 09 Apr 1998)
Revision: 2120
Log message:

Changes	Path
+13 -2	metaprl/library/library.ml
+1 -0	metaprl/library/library.mli
+12 -11	metaprl/library/orb.ml
+1 -0	metaprl/library/orb.mli
+4 -1	metaprl/library/registry.ml
+32 -1	metaprl/library/test.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-13 10:08:38 -0700 (Mon, 13 Apr 1998)
Revision: 2121
Log message:

Adding interactive proofs.

Changes	Path
Properties	metaprl/filter
+5 -2	metaprl/filter/Makefile
+22 -11	metaprl/filter/filter_bin.ml
+422 -358	metaprl/filter/filter_cache.ml
+8 -41	metaprl/filter/filter_cache.mli
Added	metaprl/filter/filter_cache_type.mlz
Properties	metaprl/filter/filter_cache_type.mlz
+26 -15	metaprl/filter/filter_parse.ml
+1292 -1147	metaprl/filter/filter_prog.ml
+7 -15	metaprl/filter/filter_prog.mli
Added	metaprl/filter/proof_type.mlz
Properties	metaprl/filter/proof_type.mlz

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-13 14:11:25 -0700 (Mon, 13 Apr 1998)
Revision: 2122
Log message:

Added interactive proofs to filter.

Changes	Path
+1 -1	metaprl/editor/ml/Makefile
+74 -125	metaprl/editor/ml/proof.ml
+6 -17	metaprl/editor/ml/proof.mli
+20 -117	metaprl/editor/ml/proof_step.ml
+7 -24	metaprl/editor/ml/proof_step.mli
+15 -15	metaprl/filter/Makefile
+19 -5	metaprl/filter/proof_type.mlz
+6 -0	metaprl/mk/config
+1 -1	metaprl/mllib/Makefile
+1 -1	metaprl/refiner/Makefile
+1 -1	metaprl/theories/base/Makefile
+1 -1	metaprl/theories/itt/Makefile
+1 -1	metaprl/theories/tactic/Makefile
+6 -13	metaprl/theories/tactic/tactic_type.mlz
+4 -0	metaprl/theories/tactic/tacticals.ml
Added	metaprl/util/Makefile
Properties	metaprl/util/Makefile
Added	metaprl/util/misc.ml
Properties	metaprl/util/misc.ml
Added	metaprl/util/misc.mli
Properties	metaprl/util/misc.mli
Added	metaprl/util/ocamldep.mll
Properties	metaprl/util/ocamldep.mll

Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 1998-04-14 12:29:42 -0700 (Tue, 14 Apr 1998)
Revision: 2123
Log message:

text filename

Changes	Path
+4 -1	metaprl/library/registry.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-15 05:40:07 -0700 (Wed, 15 Apr 1998)
Revision: 2124
Log message:

Updating editor packages to Filter_summarys.

Changes	Path
Properties	metaprl/editor/ml
+43 -41	metaprl/editor/ml/package_graph.ml
+22 -20	metaprl/editor/ml/package_graph.mli
+85 -193	metaprl/editor/ml/package_info.ml
+5 -48	metaprl/editor/ml/package_info.mli
Deleted	metaprl/editor/ml/package_io.ml
Deleted	metaprl/editor/ml/package_io.mli
Added	metaprl/editor/ml/package_type.mlz
Properties	metaprl/editor/ml/package_type.mlz
+6 -3	metaprl/editor/ml/proof_edit.ml
Properties	metaprl/filter
+0 -2	metaprl/filter/Makefile
+14 -19	metaprl/filter/filter_bin.ml
+364 -419	metaprl/filter/filter_cache.ml
+47 -4	metaprl/filter/filter_cache.mli
+8 -0	metaprl/filter/filter_cache_fun.ml
Deleted	metaprl/filter/filter_cache_type.mlz
+18 -23	metaprl/filter/filter_parse.ml
+1166 -1288	metaprl/filter/filter_prog.ml
+16 -4	metaprl/filter/filter_prog.mli
+4 -0	metaprl/filter/filter_summary_type.mlz
+18 -1	metaprl/mllib/filename_util.ml
+5 -0	metaprl/mllib/filename_util.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-15 05:41:51 -0700 (Wed, 15 Apr 1998)
Revision: 2125
Log message:

Added edit_type.mli

Changes	Path
Properties	metaprl/editor/ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-15 06:36:33 -0700 (Wed, 15 Apr 1998)
Revision: 2126
Log message:

Added .cvsignore

Changes	Path
Properties	metaprl/util

Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 1998-04-15 12:51:35 -0700 (Wed, 15 Apr 1998)
Revision: 2127
Log message:

ascii

Changes	Path
+102 -0	metaprl/library/db.ml
+5 -1	metaprl/library/db.mli
+42 -41	metaprl/library/mbterm.ml
+3 -1	metaprl/library/test.ml

Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 1998-04-15 12:53:47 -0700 (Wed, 15 Apr 1998)
Revision: 2128
Log message:

ascii

Changes	Path
+1 -1	metaprl/library/db.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-15 15:29:02 -0700 (Wed, 15 Apr 1998)
Revision: 2129
Log message:

Converting packages from summaries.

Changes	Path
+3 -3	metaprl/editor/ml/Makefile
+176 -25	metaprl/editor/ml/package_info.ml
+23 -10	metaprl/editor/ml/package_type.mlz
Deleted	metaprl/editor/ml/package_util.ml
Deleted	metaprl/editor/ml/package_util.mli
+11 -1	metaprl/filter/filter_cache_fun.ml
+20 -0	metaprl/filter/filter_summary.ml
+5 -0	metaprl/filter/filter_summary.mli
+5 -0	metaprl/filter/filter_summary_type.mlz

Changes by: Richard Eaton (eaton at cs.cornell.edu)
Date: 1998-04-15 15:59:18 -0700 (Wed, 15 Apr 1998)
Revision: 2130
Log message:

Changes	Path
+1 -0	metaprl/library/Makefile
Added	metaprl/library/ascii_scan.mli
Properties	metaprl/library/ascii_scan.mli
Added	metaprl/library/ascii_term.ml
Properties	metaprl/library/ascii_term.ml
+215 -15	metaprl/library/db.ml

Changes by: Richard Eaton (eaton at cs.cornell.edu)
Date: 1998-04-15 20:33:19 -0700 (Wed, 15 Apr 1998)
Revision: 2131
Log message:

Changes	Path
+9 -9	metaprl/library/db.ml

Changes by: Richard Eaton (eaton at cs.cornell.edu)
Date: 1998-04-16 07:55:12 -0700 (Thu, 16 Apr 1998)
Revision: 2132
Log message:

Changes	Path
Added	metaprl/library/ascii_scan.ml
Properties	metaprl/library/ascii_scan.ml
Deleted	metaprl/library/ascii_term.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-16 07:55:44 -0700 (Thu, 16 Apr 1998)
Revision: 2133
Log message:

Upgrading packages.

Changes	Path
+82 -31	metaprl/editor/ml/package_info.ml

Changes by: Richard Eaton (eaton at cs.cornell.edu)
Date: 1998-04-16 13:50:17 -0700 (Thu, 16 Apr 1998)
Revision: 2134
Log message:

Changes	Path
+25 -16	metaprl/library/ascii_scan.ml

Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 1998-04-16 14:21:21 -0700 (Thu, 16 Apr 1998)
Revision: 2135
Log message:

Changes	Path
+68 -6	metaprl/library/db.ml
+5 -2	metaprl/library/db.mli
+17 -13	metaprl/library/mbterm.ml

Changes by: Richard Eaton (eaton at cs.cornell.edu)
Date: 1998-04-16 16:18:34 -0700 (Thu, 16 Apr 1998)
Revision: 2136
Log message:

Changes	Path
+11 -3	metaprl/library/ascii_scan.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-16 18:31:36 -0700 (Thu, 16 Apr 1998)
Revision: 2137
Log message:

Editor is almost constructed.

Changes	Path
+2 -5	metaprl/editor/ml/Makefile
Deleted	metaprl/editor/ml/display_package.ml
Deleted	metaprl/editor/ml/display_package.mli
Deleted	metaprl/editor/ml/display_package_graph.ml
Deleted	metaprl/editor/ml/display_package_graph.mli
Deleted	metaprl/editor/ml/display_theory_item.ml
Deleted	metaprl/editor/ml/display_theory_item.mli
Deleted	metaprl/editor/ml/package_graph.ml
Deleted	metaprl/editor/ml/package_graph.mli
+117 -41	metaprl/editor/ml/package_info.ml
+6 -1	metaprl/editor/ml/package_type.mlz
+28 -25	metaprl/editor/ml/proof.ml
+5 -2	metaprl/editor/ml/proof.mli
+12 -9	metaprl/editor/ml/proof_step.ml
+4 -1	metaprl/editor/ml/proof_step.mli
+90 -161	metaprl/editor/ml/shell.ml
+35 -46	metaprl/editor/ml/shell.mli
Properties	metaprl/filter
+3 -2	metaprl/filter/Makefile
+13 -4	metaprl/filter/filter_cache.ml
+5 -1	metaprl/filter/filter_cache.mli
+86 -80	metaprl/filter/filter_cache_fun.ml
Added	metaprl/filter/filter_proof.ml
Properties	metaprl/filter/filter_proof.ml
Added	metaprl/filter/filter_proof.mli
Properties	metaprl/filter/filter_proof.mli
Added	metaprl/filter/filter_proof_type.mlz
Properties	metaprl/filter/filter_proof_type.mlz
+7 -2	metaprl/filter/filter_summary.ml
+4 -0	metaprl/filter/filter_summary_type.mlz
Deleted	metaprl/filter/proof_type.mlz
+4 -0	metaprl/mllib/dag.mlz
+4 -1	metaprl/mllib/imp_dag.ml
+16 -9	metaprl/refiner/term.ml
Properties	metaprl/theories/base
+2 -0	metaprl/theories/base/Makefile
+5 -0	metaprl/theories/base/base_theory.mlz
+9 -0	metaprl/theories/base/nuprl_font.ml
+6 -0	metaprl/theories/base/nuprl_font.mli
Added	metaprl/theories/base/perv.ml
Properties	metaprl/theories/base/perv.ml
Added	metaprl/theories/base/perv.mli
Properties	metaprl/theories/base/perv.mli
Added	metaprl/theories/base/summary.ml
Properties	metaprl/theories/base/summary.ml
Added	metaprl/theories/base/summary.mli
Properties	metaprl/theories/base/summary.mli
+4 -1	metaprl/theories/tactic/tactic_type.mlz
+4 -1	metaprl/theories/tactic/tacticals.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-16 19:25:32 -0700 (Thu, 16 Apr 1998)
Revision: 2138
Log message:

Implementing shell.

Changes	Path
+6 -0	metaprl/editor/ml/package_info.ml
+4 -0	metaprl/editor/ml/package_type.mlz
+35 -59	metaprl/editor/ml/shell.ml

Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 1998-04-17 08:12:52 -0700 (Fri, 17 Apr 1998)
Revision: 2139
Log message:

Changes	Path
+8 -35	metaprl/library/db.ml
+2 -1	metaprl/library/db.mli
+1 -1	metaprl/library/mbterm.ml

Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 1998-04-17 08:13:53 -0700 (Fri, 17 Apr 1998)
Revision: 2140
Log message:

Changes	Path
+2 -2	metaprl/library/db.ml
+0 -2	metaprl/library/db.mli

Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 1998-04-17 08:31:04 -0700 (Fri, 17 Apr 1998)
Revision: 2141
Log message:

Changes	Path
+1 -1	metaprl/library/db.ml

Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 1998-04-17 09:47:09 -0700 (Fri, 17 Apr 1998)
Revision: 2142
Log message:

Changes	Path
+9 -0	metaprl/library/db.ml
+1 -0	metaprl/library/db.mli
+14 -1	metaprl/library/library.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-17 13:48:40 -0700 (Fri, 17 Apr 1998)
Revision: 2143
Log message:

Updating refiner for extraction.

Changes	Path
Properties	metaprl/editor/ml
+3 -1	metaprl/editor/ml/Makefile
Added	metaprl/editor/ml/package_df.ml
Properties	metaprl/editor/ml/package_df.ml
Added	metaprl/editor/ml/package_df.mli
Properties	metaprl/editor/ml/package_df.mli
+37 -12	metaprl/editor/ml/shell.mli
Added	metaprl/editor/ml/shell_rewrite.ml
Properties	metaprl/editor/ml/shell_rewrite.ml
Added	metaprl/editor/ml/shell_rewrite.mli
Properties	metaprl/editor/ml/shell_rewrite.mli
Added	metaprl/editor/ml/shell_type.mlz
Properties	metaprl/editor/ml/shell_type.mlz
+4 -1	metaprl/filter/filter_prog.ml
+26 -0	metaprl/filter/filter_prog.mli
+92 -59	metaprl/filter/filter_summary.ml
+59 -0	metaprl/filter/filter_summary.mli
+4 -1	metaprl/filter/filter_summary_type.mlz
+18 -1	metaprl/mllib/list_util.ml
+4 -0	metaprl/mllib/list_util.mli
+15 -2	metaprl/refiner/refine.ml
+26 -1	metaprl/refiner/refine_sig.ml

Changes by: Richard Eaton (eaton at cs.cornell.edu)
Date: 1998-04-17 14:57:06 -0700 (Fri, 17 Apr 1998)
Revision: 2144
Log message:

Changes	Path
+16 -1	metaprl/library/basic.ml
+5 -0	metaprl/library/basic.mli
+255 -53	metaprl/library/db.ml
+2 -3	metaprl/library/db.mli
+1 -1	metaprl/library/orb.ml
+7 -2	metaprl/library/test.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-21 12:55:23 -0700 (Tue, 21 Apr 1998)
Revision: 2145
Log message:

Upgraded refiner for program extraction.

Changes	Path
+5 -2	metaprl/filter/filter_cache_fun.ml
+5 -2	metaprl/filter/filter_parse.ml
+87 -53	metaprl/filter/filter_prog.ml
+9 -6	metaprl/filter/filter_prog.mli
+39 -14	metaprl/filter/filter_summary.ml
+4 -1	metaprl/filter/filter_summary.mli
+4 -1	metaprl/mllib/array_util.ml
+4 -1	metaprl/mllib/array_util.mli
+95 -57	metaprl/mllib/list_util.ml
+22 -14	metaprl/mllib/list_util.mli
+938 -360	metaprl/refiner/refine.ml
+5 -0	metaprl/refiner/refine_exn.ml
+145 -73	metaprl/refiner/refine_sig.ml
+23 -16	metaprl/refiner/rewrite.ml
+4 -1	metaprl/refiner/rformat.ml
+26 -26	metaprl/refiner/term.ml
+5 -1	metaprl/refiner/term.mli
+4 -1	metaprl/theories/base/typeinf.ml
Properties	metaprl/theories/itt
+6 -1	metaprl/theories/itt/itt_equal.ml
+7 -3	metaprl/theories/itt/itt_squash.ml
+4 -1	metaprl/theories/itt/itt_subtype.ml
+12 -8	metaprl/theories/tactic/sequent.ml
+4 -1	metaprl/theories/tactic/tactic_type.mlz
+117 -78	metaprl/theories/tactic/tacticals.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-21 13:58:10 -0700 (Tue, 21 Apr 1998)
Revision: 2146
Log message:

Fixed typing problems introduced by refiner msequents.

Changes	Path
+5 -1	metaprl/editor/emacs/caml.el
+28 -17	metaprl/editor/ml/proof_step.ml
+9 -12	metaprl/editor/ml/shell_rewrite.ml
+11 -4	metaprl/filter/filter_parse.ml
+32 -15	metaprl/filter/filter_proof.ml
+8 -5	metaprl/filter/filter_proof_type.mlz
+8 -1	metaprl/theories/itt/itt_int.ml
+19 -16	metaprl/theories/tactic/tactic_cache.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-22 07:06:35 -0700 (Wed, 22 Apr 1998)
Revision: 2147
Log message:

Implementing proof editor.

Changes	Path
+12 -0	metaprl/editor/ml/proof.mli
+17 -3	metaprl/editor/ml/proof_step.ml
+12 -5	metaprl/editor/ml/proof_step.mli
+7 -4	metaprl/editor/ml/shell_rewrite.ml
+1 -0	metaprl/refiner/Makefile
+11 -40	metaprl/refiner/refine.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-22 07:14:32 -0700 (Wed, 22 Apr 1998)
Revision: 2148
Log message:

Utilities for the refiner.

Changes	Path
Added	metaprl/refiner/refine_util.ml
Properties	metaprl/refiner/refine_util.ml
Added	metaprl/refiner/refine_util.mli
Properties	metaprl/refiner/refine_util.mli

Changes by: Richard Eaton (eaton at cs.cornell.edu)
Date: 1998-04-22 11:25:10 -0700 (Wed, 22 Apr 1998)
Revision: 2149
Log message:

Changes	Path
+14 -7	metaprl/library/ascii_scan.ml
+0 -1	metaprl/library/ascii_scan.mli
+22 -10	metaprl/library/basic.ml
+1 -2	metaprl/library/basic.mli
+89 -61	metaprl/library/db.ml
+2 -0	metaprl/library/db.mli
+1 -1	metaprl/library/mathBus.ml
+1 -1	metaprl/library/mbterm.ml
+9 -12	metaprl/library/nuprl5.ml
+3 -3	metaprl/library/nuprl5.mli
+22 -3	metaprl/library/test.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-22 15:45:29 -0700 (Wed, 22 Apr 1998)
Revision: 2150
Log message:

*** empty log message ***

Changes	Path
+5 -2	metaprl/editor/ml/proof.ml
+39 -34	metaprl/editor/ml/proof.mli
+26 -13	metaprl/editor/ml/proof_step.ml
+20 -9	metaprl/editor/ml/proof_step.mli
+6 -13	metaprl/filter/filter_prog.ml
+36 -0	metaprl/filter/filter_proof.ml
+8 -0	metaprl/filter/filter_proof.mli
+5 -1	metaprl/theories/base/typeinf.ml
+5 -1	metaprl/theories/base/typeinf.mli
+5 -1	metaprl/theories/itt/itt_atom.ml
+5 -1	metaprl/theories/itt/itt_atom.mli
+12 -3	metaprl/theories/itt/itt_dfun.ml
+5 -1	metaprl/theories/itt/itt_dfun.mli
+11 -4	metaprl/theories/itt/itt_dprod.ml
+5 -1	metaprl/theories/itt/itt_dprod.mli
+8 -3	metaprl/theories/itt/itt_equal.ml
+6 -1	metaprl/theories/itt/itt_equal.mli
+11 -3	metaprl/theories/itt/itt_fun.ml
+4 -0	metaprl/theories/itt/itt_fun.mli
+11 -5	metaprl/theories/itt/itt_int.ml
+5 -1	metaprl/theories/itt/itt_int.mli
+12 -5	metaprl/theories/itt/itt_isect.ml
+5 -1	metaprl/theories/itt/itt_isect.mli
+10 -4	metaprl/theories/itt/itt_list.ml
+5 -1	metaprl/theories/itt/itt_list.mli
+9 -4	metaprl/theories/itt/itt_logic.ml
+8 -4	metaprl/theories/itt/itt_prec.ml
+4 -1	metaprl/theories/itt/itt_prec.mli
+12 -4	metaprl/theories/itt/itt_prod.ml
+4 -0	metaprl/theories/itt/itt_prod.mli
+12 -5	metaprl/theories/itt/itt_quotient.ml
+5 -1	metaprl/theories/itt/itt_quotient.mli
+14 -5	metaprl/theories/itt/itt_rfun.ml
+5 -1	metaprl/theories/itt/itt_rfun.mli
+15 -6	metaprl/theories/itt/itt_set.ml
+5 -1	metaprl/theories/itt/itt_set.mli
+6 -2	metaprl/theories/itt/itt_soft.ml
+8 -2	metaprl/theories/itt/itt_soft.mli
+7 -2	metaprl/theories/itt/itt_squash.ml
+5 -1	metaprl/theories/itt/itt_squash.mli
+7 -3	metaprl/theories/itt/itt_srec.ml
+10 -2	metaprl/theories/itt/itt_struct.ml
+6 -1	metaprl/theories/itt/itt_struct.mli
+8 -1	metaprl/theories/itt/itt_subtype.ml
+5 -1	metaprl/theories/itt/itt_subtype.mli
+12 -4	metaprl/theories/itt/itt_union.ml
+5 -1	metaprl/theories/itt/itt_union.mli
+7 -2	metaprl/theories/itt/itt_unit.ml
+5 -1	metaprl/theories/itt/itt_unit.mli
+9 -3	metaprl/theories/itt/itt_void.ml
+5 -1	metaprl/theories/itt/itt_void.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-23 13:04:52 -0700 (Thu, 23 Apr 1998)
Revision: 2151
Log message:

Initial rebuilt editor.

Changes	Path
+51 -7	metaprl/editor/ml/Makefile
Deleted	metaprl/editor/ml/edit_type.mlz
Deleted	metaprl/editor/ml/editor_init.ml
Deleted	metaprl/editor/ml/editor_init.mli
Deleted	metaprl/editor/ml/main.ml
Deleted	metaprl/editor/ml/main.mli
+16 -7	metaprl/editor/ml/package_df.ml
+15 -5	metaprl/editor/ml/package_df.mli
+6 -2	metaprl/editor/ml/package_info.ml
+4 -0	metaprl/editor/ml/package_info.mli
+429 -218	metaprl/editor/ml/proof.ml
+12 -6	metaprl/editor/ml/proof.mli
+116 -47	metaprl/editor/ml/proof_edit.ml
+23 -4	metaprl/editor/ml/proof_edit.mli
+52 -5	metaprl/editor/ml/proof_step.ml
+4 -1	metaprl/editor/ml/proof_step.mli
+120 -78	metaprl/editor/ml/shell.ml
+17 -7	metaprl/editor/ml/shell.mli
Added	metaprl/editor/ml/shell_null.ml
Properties	metaprl/editor/ml/shell_null.ml
Added	metaprl/editor/ml/shell_null.mli
Properties	metaprl/editor/ml/shell_null.mli
Added	metaprl/editor/ml/shell_p4.ml
Properties	metaprl/editor/ml/shell_p4.ml
Added	metaprl/editor/ml/shell_p4.mli
Properties	metaprl/editor/ml/shell_p4.mli
+119 -34	metaprl/editor/ml/shell_rewrite.ml
+12 -1	metaprl/editor/ml/shell_rewrite.mli
+16 -6	metaprl/editor/ml/shell_type.mlz
+3 -0	metaprl/mk/config
+16 -0	metaprl/mllib/list_util.ml
+4 -0	metaprl/mllib/list_util.mli
+5 -0	metaprl/refiner/refine_exn.mli
+10 -0	metaprl/refiner/term.ml
+6 -0	metaprl/refiner/term.mli
+4 -0	metaprl/theories/base/perv.ml
+4 -0	metaprl/theories/base/perv.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-23 19:44:07 -0700 (Thu, 23 Apr 1998)
Revision: 2152
Log message:

Added more extensive debugging capabilities.

Changes	Path
+3 -1	metaprl/clib/Makefile
Added	metaprl/clib/debug.c
Properties	metaprl/clib/debug.c
Added	metaprl/clib/debug.h
Properties	metaprl/clib/debug.h
Added	metaprl/clib/ml_debug.c
Properties	metaprl/clib/ml_debug.c
Added	metaprl/clib/ml_debug.h
Properties	metaprl/clib/ml_debug.h
+1 -1	metaprl/editor/ml/Makefile
+11 -0	metaprl/editor/ml/package_df.ml
+11 -3	metaprl/editor/ml/package_info.ml
+11 -0	metaprl/editor/ml/package_int.ml
+10 -0	metaprl/editor/ml/proof.ml
+11 -0	metaprl/editor/ml/proof_edit.ml
+11 -0	metaprl/editor/ml/proof_step.ml
+10 -0	metaprl/editor/ml/shell.ml
+11 -0	metaprl/editor/ml/shell_null.ml
+11 -0	metaprl/editor/ml/shell_rewrite.ml
+0 -1	metaprl/filter/Makefile
+11 -0	metaprl/filter/buffer.ml
+11 -0	metaprl/filter/filter_ast.ml
+9 -0	metaprl/filter/filter_bin.ml
+9 -1	metaprl/filter/filter_cache.ml
+19 -11	metaprl/filter/filter_cache_fun.ml
+11 -0	metaprl/filter/filter_comment.ml
+11 -0	metaprl/filter/filter_hash.ml
+28 -20	metaprl/filter/filter_html.ml
+9 -0	metaprl/filter/filter_main.ml
+9 -0	metaprl/filter/filter_ocaml.ml
+14 -6	metaprl/filter/filter_parse.ml
+56 -48	metaprl/filter/filter_prog.ml
+11 -0	metaprl/filter/filter_proof.ml
+9 -0	metaprl/filter/filter_summary.ml
+11 -0	metaprl/filter/filter_summary_base.ml
+10 -2	metaprl/filter/filter_summary_io.ml
+10 -2	metaprl/filter/filter_summary_util.ml
+10 -0	metaprl/filter/filter_util.ml
+10 -0	metaprl/filter/free_vars.ml
+3 -0	metaprl/filter/infix.ml
+11 -0	metaprl/filter/mLast_util.ml
+9 -0	metaprl/filter/prlcomp.ml
+13 -5	metaprl/filter/term_grammar.ml
+11 -0	metaprl/filter/term_quote.ml
+1 -0	metaprl/mllib/Makefile
+39 -4	metaprl/mllib/debug.ml
+39 -4	metaprl/mllib/debug.mli
Added	metaprl/mllib/debug_set.ml
Properties	metaprl/mllib/debug_set.ml
Added	metaprl/mllib/debug_set.mli
Properties	metaprl/mllib/debug_set.mli
+12 -9	metaprl/mllib/file_base.ml
+11 -0	metaprl/refiner/dform.ml
+11 -0	metaprl/refiner/dform_print.ml
+9 -0	metaprl/refiner/ml_file.ml
+9 -0	metaprl/refiner/ml_print.ml
+17 -0	metaprl/refiner/ml_string.ml
+10 -0	metaprl/refiner/opname.ml
+22 -13	metaprl/refiner/refine.ml
+9 -0	metaprl/refiner/refine_exn.ml
+11 -0	metaprl/refiner/refine_util.ml
+11 -1	metaprl/refiner/rewrite.ml
+10 -1	metaprl/refiner/rformat.ml
+19 -10	metaprl/refiner/simple_print.ml
+9 -0	metaprl/refiner/term.ml
+10 -0	metaprl/refiner/term_dtable.ml
+11 -0	metaprl/refiner/term_stable.ml
+10 -0	metaprl/refiner/term_table.ml
+11 -0	metaprl/refiner/term_template.ml
+9 -0	metaprl/refiner/term_util.ml
+11 -0	metaprl/refiner/theory.ml
+17 -0	metaprl/theories/base/base_dform.ml
+11 -0	metaprl/theories/base/base_dtactic.ml
+8 -0	metaprl/theories/base/evaluator.ml
+11 -0	metaprl/theories/base/nuprl_font.ml
+11 -0	metaprl/theories/base/perv.ml
+11 -0	metaprl/theories/base/summary.ml
+11 -0	metaprl/theories/base/typeinf.ml
+10 -0	metaprl/theories/itt/itt_atom.ml
+10 -0	metaprl/theories/itt/itt_dfun.ml
+10 -0	metaprl/theories/itt/itt_dprod.ml
+10 -0	metaprl/theories/itt/itt_equal.ml
+11 -0	metaprl/theories/itt/itt_ext_equal.ml
+10 -0	metaprl/theories/itt/itt_fun.ml
+10 -0	metaprl/theories/itt/itt_int.ml
+10 -0	metaprl/theories/itt/itt_isect.ml
+10 -0	metaprl/theories/itt/itt_list.ml
+10 -0	metaprl/theories/itt/itt_logic.ml
+10 -0	metaprl/theories/itt/itt_prec.ml
+10 -0	metaprl/theories/itt/itt_prod.ml
+10 -0	metaprl/theories/itt/itt_quotient.ml
+8 -0	metaprl/theories/itt/itt_redrules.ml
+10 -0	metaprl/theories/itt/itt_rfun.ml
+10 -0	metaprl/theories/itt/itt_set.ml
+10 -0	metaprl/theories/itt/itt_soft.ml
+11 -0	metaprl/theories/itt/itt_squash.ml
+10 -0	metaprl/theories/itt/itt_srec.ml
+10 -0	metaprl/theories/itt/itt_struct.ml
+10 -0	metaprl/theories/itt/itt_subtype.ml
+10 -0	metaprl/theories/itt/itt_union.ml
+10 -0	metaprl/theories/itt/itt_unit.ml
+10 -0	metaprl/theories/itt/itt_void.ml
+10 -0	metaprl/theories/itt/main.ml
+11 -0	metaprl/theories/tactic/options.ml
+11 -0	metaprl/theories/tactic/sequent.ml
+11 -0	metaprl/theories/tactic/tactic_cache.ml
+4 -0	metaprl/theories/tactic/tactic_type.mlz
+11 -0	metaprl/theories/tactic/tacticals.ml
+11 -0	metaprl/theories/tactic/var.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-24 12:39:13 -0700 (Fri, 24 Apr 1998)
Revision: 2153
Log message:

Updated debugging.

Changes	Path
+5 -1	metaprl/editor/ml/Makefile
+8 -1	metaprl/editor/ml/shell.ml
+4 -1	metaprl/filter/buffer.ml
+4 -1	metaprl/filter/filter_ast.ml
+4 -1	metaprl/filter/filter_bin.ml
+4 -1	metaprl/filter/filter_cache.ml
+4 -1	metaprl/filter/filter_cache_fun.ml
+4 -1	metaprl/filter/filter_comment.ml
+4 -1	metaprl/filter/filter_hash.ml
+4 -1	metaprl/filter/filter_html.ml
+4 -1	metaprl/filter/filter_main.ml
+4 -1	metaprl/filter/filter_ocaml.ml
+4 -1	metaprl/filter/filter_parse.ml
+29 -4	metaprl/filter/filter_prog.ml
+4 -1	metaprl/filter/filter_proof.ml
+4 -1	metaprl/filter/filter_summary.ml
+4 -1	metaprl/filter/filter_summary_base.ml
+4 -1	metaprl/filter/filter_summary_io.ml
+4 -1	metaprl/filter/filter_summary_util.ml
+4 -1	metaprl/filter/filter_util.ml
+4 -1	metaprl/filter/free_vars.ml
+4 -1	metaprl/filter/mLast_util.ml
+4 -1	metaprl/filter/prlcomp.ml
+4 -1	metaprl/filter/term_grammar.ml
+4 -1	metaprl/filter/term_quote.ml
+11 -0	metaprl/mllib/array_util.ml
+11 -0	metaprl/mllib/bitset.ml
+11 -0	metaprl/mllib/ctype.ml
+9 -0	metaprl/mllib/debug_set.ml
+10 -0	metaprl/mllib/env_arg.ml
+9 -0	metaprl/mllib/file_base.ml
+11 -0	metaprl/mllib/file_type_base.ml
+11 -0	metaprl/mllib/file_util.ml
+11 -0	metaprl/mllib/filename_util.ml
+11 -0	metaprl/mllib/imp_dag.ml
+11 -0	metaprl/mllib/list_util.ml
+11 -0	metaprl/mllib/precedence.ml
+11 -0	metaprl/mllib/ref_util.ml
+11 -0	metaprl/mllib/string_util.ml
+3 -6	metaprl/refiner/ml_string.ml
+4 -7	metaprl/theories/base/base_dform.ml
+4 -1	metaprl/theories/base/base_dtactic.ml
+1 -1	metaprl/theories/base/evaluator.ml
+4 -1	metaprl/theories/base/nuprl_font.ml
+4 -1	metaprl/theories/base/perv.ml
+4 -1	metaprl/theories/base/summary.ml
+4 -1	metaprl/theories/base/typeinf.ml

Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 1998-04-27 06:25:47 -0700 (Mon, 27 Apr 1998)
Revision: 2154
Log message:

ascii

Changes	Path
+38 -17	metaprl/library/db.ml
+21 -4	metaprl/library/library.ml
+1 -1	metaprl/library/mathBus.mli
+14 -10	metaprl/library/mbterm.ml
+19 -2	metaprl/library/test.ml

Changes by: Richard Eaton (eaton at cs.cornell.edu)
Date: 1998-04-27 12:18:21 -0700 (Mon, 27 Apr 1998)
Revision: 2155
Log message:

Changes	Path
+2 -1	metaprl/library/ascii_scan.ml
+40 -11	metaprl/library/db.ml
+4 -7	metaprl/library/test.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-28 11:31:05 -0700 (Tue, 28 Apr 1998)
Revision: 2156
Log message:

ls() works, adding display.

Changes	Path
+12 -13	metaprl/editor/ml/Makefile
Added	metaprl/editor/ml/nl.ml
Properties	metaprl/editor/ml/nl.ml
Added	metaprl/editor/ml/nl.mli
Properties	metaprl/editor/ml/nl.mli
+98 -38	metaprl/editor/ml/package_info.ml
+16 -1	metaprl/editor/ml/package_type.mlz
+6 -3	metaprl/editor/ml/proof.ml
+6 -2	metaprl/editor/ml/proof.mli
+5 -2	metaprl/editor/ml/proof_edit.ml
+4 -1	metaprl/editor/ml/proof_edit.mli
+11 -5	metaprl/editor/ml/proof_step.ml
+5 -1	metaprl/editor/ml/proof_step.mli
+218 -65	metaprl/editor/ml/shell.ml
+13 -0	metaprl/editor/ml/shell.mli
+96 -0	metaprl/editor/ml/shell_p4.ml
+18 -0	metaprl/editor/ml/shell_p4.mli
+5 -2	metaprl/editor/ml/shell_rewrite.ml
+4 -1	metaprl/editor/ml/shell_type.mlz
+5 -5	metaprl/filter/Makefile
Added	metaprl/filter/filter_exn.ml
Properties	metaprl/filter/filter_exn.ml
Added	metaprl/filter/filter_exn.mli
Properties	metaprl/filter/filter_exn.mli
+5 -0	metaprl/filter/filter_parse.ml
+3 -1	metaprl/filter/filter_parse.mli
+41 -17	metaprl/filter/filter_prog.ml
+6 -1	metaprl/filter/prlcomp.ml
+4 -1	metaprl/mk/config
+7 -0	metaprl/mllib/debug.ml
+7 -0	metaprl/mllib/debug.mli
+9 -0	metaprl/mllib/debug_set.ml
+4 -0	metaprl/mllib/debug_set.mli
+8 -0	metaprl/mllib/list_util.ml
+5 -0	metaprl/mllib/list_util.mli
+8 -4	metaprl/mllib/string_util.ml
+1 -1	metaprl/refiner/Makefile
+5 -1	metaprl/refiner/dform.ml
+7 -29	metaprl/refiner/dform_print.ml
+3 -18	metaprl/refiner/dform_print.mli
+3 -2	metaprl/refiner/refine.ml
+219 -74	metaprl/refiner/refine_exn.ml
+12 -2	metaprl/refiner/refine_exn.mli
+11 -8	metaprl/refiner/refine_sig.ml
+18 -8	metaprl/refiner/rformat.ml
+6 -2	metaprl/refiner/term_table.ml
+57 -1	metaprl/refiner/term_template.ml
+37 -1	metaprl/refiner/theory.ml
+8 -0	metaprl/refiner/theory.mli
+4 -0	metaprl/theories/base/Makefile
+32 -29	metaprl/theories/base/base_dform.ml
+31 -13	metaprl/theories/base/summary.ml
+5 -0	metaprl/theories/base/summary.mli
+3 -0	metaprl/theories/itt/Makefile
+1 -0	metaprl/theories/tactic/Makefile

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-28 12:24:15 -0700 (Tue, 28 Apr 1998)
Revision: 2157
Log message:

Added -prl option.

Changes	Path
+24 -1	metaprl/util/ocamldep.mll

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-28 14:38:13 -0700 (Tue, 28 Apr 1998)
Revision: 2158
Log message:

Adjusted uppercasing.

Changes	Path
+4 -1	metaprl/filter/filter_cache.ml
+4 -1	metaprl/filter/filter_proof.ml
+4 -1	metaprl/filter/filter_summary.ml
+47 -45	metaprl/mllib/debug.ml
+5 -1	metaprl/refiner/term.ml
+9 -2	metaprl/refiner/term_table.ml
+34 -32	metaprl/refiner/term_template.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-29 07:50:25 -0700 (Wed, 29 Apr 1998)
Revision: 2159
Log message:

Added ocaml_sos.

Changes	Path
+3 -1	metaprl/editor/ml/Makefile
+4 -4	metaprl/filter/Makefile
+6 -1	metaprl/filter/filter_ocaml.ml
+5 -2	metaprl/filter/filter_summary.ml
+1 -1	metaprl/library/Makefile
+1 -1	metaprl/mk/config
+5 -4	metaprl/mllib/list_util.ml
+75 -36	metaprl/refiner/dform.ml
+13 -17	metaprl/refiner/refine.ml
+19 -11	metaprl/refiner/rewrite.ml
+6 -2	metaprl/refiner/rewrite.mli
+14 -4	metaprl/refiner/term.ml
+4 -0	metaprl/refiner/term.mli
+37 -23	metaprl/refiner/term_dtable.ml
+19 -17	metaprl/refiner/term_dtable.mli
+43 -24	metaprl/refiner/term_table.ml
+6 -3	metaprl/refiner/term_table.mli
+27 -6	metaprl/refiner/term_template.ml
+6 -2	metaprl/refiner/term_template.mli
+1 -1	metaprl/theories/base/Makefile
+11 -2	metaprl/theories/base/summary.ml
+5 -0	metaprl/theories/base/summary.mli
+5 -2	metaprl/theories/base/typeinf.ml
+6 -12	metaprl/theories/ocaml/Makefile
+8 -0	metaprl/theories/ocaml/ocaml_base_df.ml
Deleted	metaprl/theories/ocaml/ocaml_base_sos.ml
Deleted	metaprl/theories/ocaml/ocaml_base_sos.mli
Added	metaprl/theories/ocaml/ocaml_df.ml
Properties	metaprl/theories/ocaml/ocaml_df.ml
Added	metaprl/theories/ocaml/ocaml_df.mli
Properties	metaprl/theories/ocaml/ocaml_df.mli
+7 -5	metaprl/theories/ocaml/ocaml_df.mlz
+8 -0	metaprl/theories/ocaml/ocaml_expr_df.ml
Deleted	metaprl/theories/ocaml/ocaml_expr_sos.ml
Deleted	metaprl/theories/ocaml/ocaml_expr_sos.mli
Deleted	metaprl/theories/ocaml/ocaml_logic.ml
Deleted	metaprl/theories/ocaml/ocaml_logic.mli
+8 -0	metaprl/theories/ocaml/ocaml_me_df.ml
Deleted	metaprl/theories/ocaml/ocaml_me_sos.ml
Deleted	metaprl/theories/ocaml/ocaml_me_sos.mli
+9 -0	metaprl/theories/ocaml/ocaml_mt_df.ml
Deleted	metaprl/theories/ocaml/ocaml_mt_sos.ml
Deleted	metaprl/theories/ocaml/ocaml_mt_sos.mli
+11 -3	metaprl/theories/ocaml/ocaml_patt_df.ml
Deleted	metaprl/theories/ocaml/ocaml_patt_sos.ml
Deleted	metaprl/theories/ocaml/ocaml_patt_sos.mli
+8 -0	metaprl/theories/ocaml/ocaml_sig_df.ml
Deleted	metaprl/theories/ocaml/ocaml_sig_sos.ml
Deleted	metaprl/theories/ocaml/ocaml_sig_sos.mli
+9 -1	metaprl/theories/ocaml/ocaml_str_df.ml
Deleted	metaprl/theories/ocaml/ocaml_str_sos.ml
Deleted	metaprl/theories/ocaml/ocaml_str_sos.mli
+9 -0	metaprl/theories/ocaml/ocaml_type_df.ml
Deleted	metaprl/theories/ocaml/ocaml_type_sos.ml
Deleted	metaprl/theories/ocaml/ocaml_type_sos.mli
Properties	metaprl/theories/ocaml_sos
Added	metaprl/theories/ocaml_sos/Makefile
Properties	metaprl/theories/ocaml_sos/Makefile
Added	metaprl/theories/ocaml_sos/ocaml_base_sos.ml
Properties	metaprl/theories/ocaml_sos/ocaml_base_sos.ml
Added	metaprl/theories/ocaml_sos/ocaml_base_sos.mli
Properties	metaprl/theories/ocaml_sos/ocaml_base_sos.mli
Added	metaprl/theories/ocaml_sos/ocaml_expr_sos.ml
Properties	metaprl/theories/ocaml_sos/ocaml_expr_sos.ml
Added	metaprl/theories/ocaml_sos/ocaml_expr_sos.mli
Properties	metaprl/theories/ocaml_sos/ocaml_expr_sos.mli
Added	metaprl/theories/ocaml_sos/ocaml_logic.ml
Properties	metaprl/theories/ocaml_sos/ocaml_logic.ml
Added	metaprl/theories/ocaml_sos/ocaml_logic.mli
Properties	metaprl/theories/ocaml_sos/ocaml_logic.mli
Added	metaprl/theories/ocaml_sos/ocaml_me_sos.ml
Properties	metaprl/theories/ocaml_sos/ocaml_me_sos.ml
Added	metaprl/theories/ocaml_sos/ocaml_me_sos.mli
Properties	metaprl/theories/ocaml_sos/ocaml_me_sos.mli
Added	metaprl/theories/ocaml_sos/ocaml_mt_sos.ml
Properties	metaprl/theories/ocaml_sos/ocaml_mt_sos.ml
Added	metaprl/theories/ocaml_sos/ocaml_mt_sos.mli
Properties	metaprl/theories/ocaml_sos/ocaml_mt_sos.mli
Added	metaprl/theories/ocaml_sos/ocaml_patt_sos.ml
Properties	metaprl/theories/ocaml_sos/ocaml_patt_sos.ml
Added	metaprl/theories/ocaml_sos/ocaml_patt_sos.mli
Properties	metaprl/theories/ocaml_sos/ocaml_patt_sos.mli
Added	metaprl/theories/ocaml_sos/ocaml_sig_sos.ml
Properties	metaprl/theories/ocaml_sos/ocaml_sig_sos.ml
Added	metaprl/theories/ocaml_sos/ocaml_sig_sos.mli
Properties	metaprl/theories/ocaml_sos/ocaml_sig_sos.mli
Added	metaprl/theories/ocaml_sos/ocaml_str_sos.ml
Properties	metaprl/theories/ocaml_sos/ocaml_str_sos.ml
Added	metaprl/theories/ocaml_sos/ocaml_str_sos.mli
Properties	metaprl/theories/ocaml_sos/ocaml_str_sos.mli
Added	metaprl/theories/ocaml_sos/ocaml_theory.mlz
Properties	metaprl/theories/ocaml_sos/ocaml_theory.mlz
Added	metaprl/theories/ocaml_sos/ocaml_type_sos.ml
Properties	metaprl/theories/ocaml_sos/ocaml_type_sos.ml
Added	metaprl/theories/ocaml_sos/ocaml_type_sos.mli
Properties	metaprl/theories/ocaml_sos/ocaml_type_sos.mli
+58 -57	metaprl/theories/tactic/tactic_cache.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-29 13:54:17 -0700 (Wed, 29 Apr 1998)
Revision: 2160
Log message:

Initial working display forms.

Changes	Path
+2 -1	metaprl/editor/ml/Makefile
+7 -2	metaprl/editor/ml/package_df.ml
Added	metaprl/editor/ml/test.ml
Properties	metaprl/editor/ml/test.ml
Added	metaprl/editor/ml/test.mli
Properties	metaprl/editor/ml/test.mli
+32 -14	metaprl/filter/filter_parse.ml
+15 -11	metaprl/filter/filter_prog.ml
+20 -21	metaprl/filter/filter_summary.ml
+5 -1	metaprl/filter/filter_summary.mli
+79 -46	metaprl/refiner/dform.ml
+5 -1	metaprl/refiner/dform.mli
+4 -3	metaprl/refiner/term.ml
+25 -17	metaprl/refiner/term_table.ml
+9 -2	metaprl/refiner/term_template.ml
+5 -0	metaprl/refiner/term_template.mli
+0 -1	metaprl/theories/base/Makefile
+35 -32	metaprl/theories/base/base_dform.ml
+3 -1	metaprl/theories/base/base_theory.mlz
+78 -75	metaprl/theories/base/nuprl_font.ml
Deleted	metaprl/theories/base/perv.ml
Deleted	metaprl/theories/base/perv.mli
+43 -36	metaprl/theories/base/summary.ml
+1 -0	metaprl/theories/ocaml/Makefile
+4 -2	metaprl/theories/ocaml/ocaml.mlz
+65 -62	metaprl/theories/ocaml/ocaml_base_df.ml
+6 -2	metaprl/theories/ocaml/ocaml_df.ml
+6 -2	metaprl/theories/ocaml/ocaml_df.mli
+5 -1	metaprl/theories/ocaml/ocaml_df.mlz
+53 -58	metaprl/theories/ocaml/ocaml_expr_df.ml
+12 -9	metaprl/theories/ocaml/ocaml_me_df.ml
+14 -11	metaprl/theories/ocaml/ocaml_mt_df.ml
+56 -53	metaprl/theories/ocaml/ocaml_patt_df.ml
+20 -17	metaprl/theories/ocaml/ocaml_sig_df.ml
+11 -8	metaprl/theories/ocaml/ocaml_str_df.ml
+25 -22	metaprl/theories/ocaml/ocaml_type_df.ml
Added	metaprl/theories/ocaml/perv.ml
Properties	metaprl/theories/ocaml/perv.ml
Added	metaprl/theories/ocaml/perv.mli
Properties	metaprl/theories/ocaml/perv.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-30 07:20:34 -0700 (Thu, 30 Apr 1998)
Revision: 2161
Log message:

Updating term_table.

Changes	Path
Added	metaprl/editor/ml/make1
Properties	metaprl/editor/ml/make1
+5 -0	metaprl/editor/ml/test.ml
+7 -4	metaprl/filter/filter_ocaml.ml
+5 -2	metaprl/filter/filter_summary.ml
+9 -2	metaprl/refiner/dform.ml
+4 -1	metaprl/refiner/term_table.ml
+4 -1	metaprl/theories/base/summary.ml
+4 -1	metaprl/theories/ocaml/ocaml_df.ml
+6 -1	metaprl/theories/ocaml/ocaml_str_df.ml

Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 1998-04-30 07:55:29 -0700 (Thu, 30 Apr 1998)
Revision: 2162
Log message:

Changes	Path
+1 -1	metaprl/library/basic.ml
+11 -12	metaprl/library/db.ml
+16 -1	metaprl/library/library.ml
+5 -2	metaprl/library/link.ml
+12 -6	metaprl/library/mathBus.ml
+23 -22	metaprl/library/mbterm.ml
+2 -0	metaprl/library/mbterm.mli
+2 -2	metaprl/library/test.ml