Commit log for MetaPRL

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-05-01 07:59:53 -0700 (Fri, 01 May 1998)
Revision: 2163
Log message:

Updating display forms.

Changes	Path
+1 -0	metaprl/editor/ml/make1
+5 -1	metaprl/editor/ml/test.ml
+4 -1	metaprl/filter/filter_ocaml.ml
+7 -0	metaprl/mllib/debug.ml
+7 -0	metaprl/mllib/debug.mli
+4 -0	metaprl/mllib/debug_set.ml
+34 -52	metaprl/refiner/dform.ml
+35 -19	metaprl/refiner/term.ml
+4 -1	metaprl/refiner/term.mli
+298 -107	metaprl/refiner/term_table.ml
+6 -3	metaprl/refiner/term_table.mli
+5 -2	metaprl/theories/base/typeinf.ml
+5 -0	metaprl/theories/ocaml/ocaml.mlz
+69 -21	metaprl/theories/ocaml/ocaml_expr_df.ml
+24 -7	metaprl/theories/ocaml/ocaml_str_df.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-05-01 11:43:42 -0700 (Fri, 01 May 1998)
Revision: 2164
Log message:

Added raw display.

Changes	Path
+10 -0	metaprl/Makefile
+88 -74	metaprl/refiner/dform.ml
+9 -6	metaprl/refiner/term_template.ml
+4 -1	metaprl/theories/base/base_dform.ml
+8 -3	metaprl/theories/base/summary.ml
+4 -1	metaprl/theories/ocaml/ocaml_df.mli
+11 -8	metaprl/theories/ocaml/ocaml_expr_df.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-05-04 06:01:40 -0700 (Mon, 04 May 1998)
Revision: 2165
Log message:

Ocaml display without let rec.

Changes	Path
+5 -2	metaprl/editor/ml/package_df.ml
+4 -0	metaprl/editor/ml/package_type.mlz
+38 -13	metaprl/editor/ml/test.ml
+5 -1	metaprl/editor/ml/test.mli
+4 -1	metaprl/filter/filter_cache.ml
+444 -197	metaprl/filter/filter_ocaml.ml
+6 -6	metaprl/filter/filter_ocaml.mli
+4 -1	metaprl/filter/filter_proof.ml
+14 -9	metaprl/refiner/dform.ml
+166 -67	metaprl/refiner/rformat.ml
+8 -5	metaprl/refiner/term_table.ml
+8 -3	metaprl/theories/base/summary.ml
+21 -0	metaprl/theories/ocaml/ocaml.mlz
+65 -54	metaprl/theories/ocaml/ocaml_base_df.ml
+34 -27	metaprl/theories/ocaml/ocaml_base_df.mli
+127 -41	metaprl/theories/ocaml/ocaml_expr_df.ml
+4 -0	metaprl/theories/ocaml/ocaml_expr_df.mli
+5 -2	metaprl/theories/ocaml/ocaml_me_df.ml
+33 -10	metaprl/theories/ocaml/ocaml_mt_df.ml
+131 -70	metaprl/theories/ocaml/ocaml_patt_df.ml
+44 -30	metaprl/theories/ocaml/ocaml_sig_df.ml
+32 -10	metaprl/theories/ocaml/ocaml_str_df.ml
+98 -33	metaprl/theories/ocaml/ocaml_type_df.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-05-04 16:46:19 -0700 (Mon, 04 May 1998)
Revision: 2166
Log message:

Most display forms now work.

Changes	Path
+9 -3	metaprl/editor/ml/shell.ml
+10 -22	metaprl/editor/ml/test.ml
+51 -8	metaprl/filter/filter_ocaml.ml
+5 -0	metaprl/theories/ocaml/ocaml.mlz
+6 -3	metaprl/theories/ocaml/ocaml_expr_df.ml
+30 -4	metaprl/theories/ocaml/ocaml_patt_df.ml
+10 -0	metaprl/theories/ocaml/ocaml_str_df.ml

Changes by: Richard Eaton (eaton at cs.cornell.edu)
Date: 1998-05-05 13:05:57 -0700 (Tue, 05 May 1998)
Revision: 2167
Log message:

Changes	Path
+2 -1	metaprl/library/Makefile
+4 -4	metaprl/library/ascii_scan.ml
+68 -21	metaprl/library/basic.ml
+13 -0	metaprl/library/basic.mli
+18 -19	metaprl/library/db.ml
+29 -16	metaprl/library/definition.ml
+18 -7	metaprl/library/library.ml
+1 -0	metaprl/library/library.mli
Added	metaprl/library/library_eval.ml
Properties	metaprl/library/library_eval.ml
Added	metaprl/library/library_eval.mli
Properties	metaprl/library/library_eval.mli
+7 -1	metaprl/library/library_type_base.ml
+5 -0	metaprl/library/object_id.ml
+1 -0	metaprl/library/object_id.mli
+12 -5	metaprl/library/oidtable.ml
+29 -26	metaprl/library/orb.ml
+19 -10	metaprl/library/tentfunctor.ml
+1 -1	metaprl/library/tentfunctor.mli
+20 -3	metaprl/library/test.ml
+1 -0	metaprl/library/utils.ml
+1 -0	metaprl/library/utils.mli

Changes by: Richard Eaton (eaton at cs.cornell.edu)
Date: 1998-05-05 13:16:51 -0700 (Tue, 05 May 1998)
Revision: 2168
Log message:

Changes	Path
+5 -5	metaprl/library/library_eval.ml
+4 -2	metaprl/library/library_eval.mli
+1 -1	metaprl/library/test.ml

Changes by: Richard Eaton (eaton at cs.cornell.edu)
Date: 1998-05-06 11:22:43 -0700 (Wed, 06 May 1998)
Revision: 2169
Log message:

Changes	Path
+7 -0	metaprl/library/library_eval.ml
+27 -12	metaprl/library/library_eval.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-05-06 17:00:43 -0700 (Wed, 06 May 1998)
Revision: 2170
Log message:

The right paths to prlc, ocamldep, etc in Makefiles

Changes	Path
+9 -9	metaprl/Makefile
+1 -0	metaprl/editor/ml/Makefile
+2 -2	metaprl/filter/Makefile
+3 -3	metaprl/mk/config
+1 -0	metaprl/theories/base/Makefile
+1 -0	metaprl/theories/ocaml/Makefile
+1 -0	metaprl/theories/ocaml_sos/Makefile
+1 -0	metaprl/theories/rewrite/Makefile
+1 -0	metaprl/theories/tactic/Makefile
+5 -2	metaprl/util/Makefile

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-05-07 09:03:13 -0700 (Thu, 07 May 1998)
Revision: 2171
Log message:

Adding interactive proofs.

Changes	Path
+9 -2	metaprl/editor/ml/shell.ml
+57 -16	metaprl/editor/ml/shell_rewrite.ml
+22 -0	metaprl/editor/ml/shell_rewrite.mli
+31 -5	metaprl/filter/filter_bin.ml
+78 -53	metaprl/filter/filter_cache.ml
+42 -26	metaprl/filter/filter_cache.mli
+32 -8	metaprl/filter/filter_parse.ml
+918 -808	metaprl/filter/filter_prog.ml
+35 -28	metaprl/filter/filter_prog.mli
+33 -2	metaprl/filter/filter_summary.ml
+6 -0	metaprl/filter/filter_summary.mli
+14 -11	metaprl/refiner/opname.mli
+1 -0	metaprl/theories/base/Makefile
Added	metaprl/theories/base/base_cache.ml
Properties	metaprl/theories/base/base_cache.ml
Added	metaprl/theories/base/base_cache.mli
Properties	metaprl/theories/base/base_cache.mli
+13 -11	metaprl/theories/base/base_dtactic.mli
+4 -0	metaprl/theories/base/base_theory.mlz
+174 -110	metaprl/theories/base/nuprl_font.ml
+62 -28	metaprl/theories/base/nuprl_font.mli
+4 -1	metaprl/theories/base/summary.ml
+5 -0	metaprl/theories/ocaml/perv.ml
+40 -11	metaprl/theories/tactic/tactic_cache.ml
+29 -26	metaprl/theories/tactic/tactic_cache.mli
+4 -1	metaprl/theories/tactic/tactic_type.mlz

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-05-18 11:28:10 -0700 (Mon, 18 May 1998)
Revision: 2172
Log message:

      Removed standardize_apart function, compare_* functions
          and BadParamMatch exception

Changes	Path
+4 -6	metaprl/refiner/refine_exn.ml
+4 -326	metaprl/refiner/term.ml
+4 -13	metaprl/refiner/term.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-05-18 11:58:11 -0700 (Mon, 18 May 1998)
Revision: 2173
Log message:

      Use "cp -pf" instead of "install" to keep the timestamp
      and prevent unnecessary recompiling.

Changes	Path
+1 -1	metaprl/mk/config

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-05-18 13:44:29 -0700 (Mon, 18 May 1998)
Revision: 2174
Log message:

      This is the initial checkin of Term_ds module. I've got the interface and
      I am starting rewriting the implementation. Most of the code is still the "old"
      code from the Term module, and would not compile.

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

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-05-19 10:47:51 -0700 (Tue, 19 May 1998)
Revision: 2175
Log message:

      Continuing to rewrite implementation of terms in Term_ds.
      Splited Term_ds into Term_ds and Term_ds_simple

Changes	Path
+66 -597	metaprl/refiner/term_ds.ml
+28 -107	metaprl/refiner/term_ds.mli
Added	metaprl/refiner/term_ds_simple.ml
Properties	metaprl/refiner/term_ds_simple.ml
Added	metaprl/refiner/term_ds_simple.mli
Properties	metaprl/refiner/term_ds_simple.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-05-22 12:03:04 -0700 (Fri, 22 May 1998)
Revision: 2176
Log message:

Fixed a typo in rev_assoc

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

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-05-23 12:41:11 -0700 (Sat, 23 May 1998)
Revision: 2177
Log message:

Initial rewrite of term_ds is finished

Changes	Path
+349 -863	metaprl/refiner/term_ds.ml
+7 -59	metaprl/refiner/term_ds.mli
+245 -4	metaprl/refiner/term_ds_simple.ml
+50 -0	metaprl/refiner/term_ds_simple.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-05-24 22:19:12 -0700 (Sun, 24 May 1998)
Revision: 2178
Log message:

Fixed more typos

Changes	Path
+19 -16	metaprl/refiner/term.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-05-24 22:21:21 -0700 (Sun, 24 May 1998)
Revision: 2179
Log message:

Finished the initial version of Term_ds and Term_ds_simple

Changes	Path
+2 -0	metaprl/refiner/Makefile
+7 -7	metaprl/refiner/term_ds.ml
+5 -0	metaprl/refiner/term_ds.mli
+615 -461	metaprl/refiner/term_ds_simple.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-05-25 08:22:31 -0700 (Mon, 25 May 1998)
Revision: 2180
Log message:

Use == for comparing opnames

Changes	Path
+21 -18	metaprl/refiner/term.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-05-25 17:32:17 -0700 (Mon, 25 May 1998)
Revision: 2181
Log message:

Added old evaluator functions

Changes	Path
+108 -0	metaprl/refiner/term_ds_simple.ml
+21 -0	metaprl/refiner/term_ds_simple.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-05-25 17:34:35 -0700 (Mon, 25 May 1998)
Revision: 2182
Log message:

      This is an alternative implementation of a term module
      that uses delayed substitution

Changes	Path
+1402 -1536	metaprl/refiner/term.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-05-26 20:41:33 -0700 (Tue, 26 May 1998)
Revision: 2183
Log message:

Changed to match TermSig and TermSimpleSig

Changes	Path
+25 -10	metaprl/refiner/term_ds.ml
+29 -14	metaprl/refiner/term_ds.mli
+1 -1	metaprl/refiner/term_ds_simple.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-05-27 08:15:13 -0700 (Wed, 27 May 1998)
Revision: 2184
Log message:

Functorized the refiner over the Term module.

Changes	Path
+1 -0	metaprl/clib/Makefile
Added	metaprl/clib/truncate.c
Properties	metaprl/clib/truncate.c
+5 -2	metaprl/filter/filter_ast.mli
+6 -1	metaprl/filter/filter_cache.ml
+4 -1	metaprl/filter/filter_cache.mli
+4 -1	metaprl/filter/filter_cache_fun.ml
+4 -1	metaprl/filter/filter_cache_fun.mli
+5 -2	metaprl/filter/filter_html.ml
+4 -1	metaprl/filter/filter_html.mli
+7 -1	metaprl/filter/filter_ocaml.ml
+4 -1	metaprl/filter/filter_ocaml.mli
+13 -8	metaprl/filter/filter_parse.ml
+4 -1	metaprl/filter/filter_parse.mli
+45 -35	metaprl/filter/filter_prog.ml
+4 -1	metaprl/filter/filter_prog.mli
+7 -2	metaprl/filter/filter_proof.ml
+4 -1	metaprl/filter/filter_proof.mli
+5 -2	metaprl/filter/filter_proof_type.mlz
+8 -2	metaprl/filter/filter_summary.ml
+5 -2	metaprl/filter/filter_summary.mli
+4 -1	metaprl/filter/filter_summary_io.ml
+4 -1	metaprl/filter/filter_summary_io.mli
+4 -1	metaprl/filter/filter_summary_type.mlz
+4 -1	metaprl/filter/filter_summary_util.ml
+4 -1	metaprl/filter/filter_summary_util.mli
+6 -2	metaprl/filter/filter_type.mlz
+8 -4	metaprl/filter/filter_util.ml
+5 -2	metaprl/filter/filter_util.mli
+7 -2	metaprl/filter/term_grammar.ml
+5 -2	metaprl/filter/term_grammar.mli
+3 -3	metaprl/library/basic.ml
+1 -1	metaprl/library/basic.mli
+13 -12	metaprl/library/db.ml
+1 -1	metaprl/library/db.mli
+1 -1	metaprl/library/definition.ml
+1 -1	metaprl/library/definition.mli
+2 -1	metaprl/library/library.ml
+1 -1	metaprl/library/library.mli
+1 -1	metaprl/library/library_eval.ml
+1 -1	metaprl/library/library_eval.mli
+4 -1	metaprl/library/library_type_base.ml
+4 -1	metaprl/library/library_type_base.mli
+2 -2	metaprl/library/link.ml
+1 -1	metaprl/library/link.mli
+11 -11	metaprl/library/mbterm.ml
+1 -1	metaprl/library/mbterm.mli
+7 -7	metaprl/library/nuprl5.ml
+1 -1	metaprl/library/nuprl5.mli
+1 -1	metaprl/library/oidtable.ml
+1 -1	metaprl/library/oidtable.mli
+2 -1	metaprl/library/orb.ml
+1 -1	metaprl/library/orb.mli
+1 -1	metaprl/library/test.ml
Properties	metaprl/refiner
+35 -9	metaprl/refiner/Makefile
+7 -3	metaprl/refiner/dform.ml
+6 -3	metaprl/refiner/dform.mli
+5 -2	metaprl/refiner/dform_print.mli
+5 -2	metaprl/refiner/ml_file.ml
+5 -2	metaprl/refiner/ml_format_sig.ml
+5 -2	metaprl/refiner/ml_print.ml
+5 -2	metaprl/refiner/ml_print_sig.ml
+135 -102	metaprl/refiner/refine.ml
+27 -1	metaprl/refiner/refine.mli
+9 -4	metaprl/refiner/refine_exn.ml
+5 -2	metaprl/refiner/refine_exn.mli
+83 -79	metaprl/refiner/refine_sig.ml
Deleted	metaprl/refiner/refine_util.ml
Deleted	metaprl/refiner/refine_util.mli
Added	metaprl/refiner/refiner.ml
Properties	metaprl/refiner/refiner.ml
Added	metaprl/refiner/refiner.mli
Properties	metaprl/refiner/refiner.mli
Added	metaprl/refiner/refiner_sig.ml
Properties	metaprl/refiner/refiner_sig.ml
Added	metaprl/refiner/refiner_std.ml
Properties	metaprl/refiner/refiner_std.ml
Added	metaprl/refiner/refiner_std.mli
Properties	metaprl/refiner/refiner_std.mli
+1163 -1484	metaprl/refiner/rewrite.ml
+23 -75	metaprl/refiner/rewrite.mli
Added	metaprl/refiner/rewrite_sig.ml
Properties	metaprl/refiner/rewrite_sig.ml
+8 -6	metaprl/refiner/simple_print.ml
+6 -57	metaprl/refiner/simple_print.mli
Deleted	metaprl/refiner/term.ml
Deleted	metaprl/refiner/term.mli
Added	metaprl/refiner/term_addr_sig.ml
Properties	metaprl/refiner/term_addr_sig.ml
Added	metaprl/refiner/term_addr_std.ml
Properties	metaprl/refiner/term_addr_std.ml
Added	metaprl/refiner/term_addr_std.mli
Properties	metaprl/refiner/term_addr_std.mli
+6 -3	metaprl/refiner/term_dtable.ml
+4 -1	metaprl/refiner/term_dtable.mli
Added	metaprl/refiner/term_eval_sig.ml
Properties	metaprl/refiner/term_eval_sig.ml
Added	metaprl/refiner/term_eval_std.ml
Properties	metaprl/refiner/term_eval_std.ml
Added	metaprl/refiner/term_eval_std.mli
Properties	metaprl/refiner/term_eval_std.mli
Added	metaprl/refiner/term_man_sig.ml
Properties	metaprl/refiner/term_man_sig.ml
Added	metaprl/refiner/term_man_std.ml
Properties	metaprl/refiner/term_man_std.ml
Added	metaprl/refiner/term_man_std.mli
Properties	metaprl/refiner/term_man_std.mli
Added	metaprl/refiner/term_meta_sig.ml
Properties	metaprl/refiner/term_meta_sig.ml
Added	metaprl/refiner/term_meta_std.ml
Properties	metaprl/refiner/term_meta_std.ml
Added	metaprl/refiner/term_meta_std.mli
Properties	metaprl/refiner/term_meta_std.mli
Added	metaprl/refiner/term_op_sig.ml
Properties	metaprl/refiner/term_op_sig.ml
Added	metaprl/refiner/term_op_std.ml
Properties	metaprl/refiner/term_op_std.ml
Added	metaprl/refiner/term_op_std.mli
Properties	metaprl/refiner/term_op_std.mli
Added	metaprl/refiner/term_shape_sig.ml
Properties	metaprl/refiner/term_shape_sig.ml
Added	metaprl/refiner/term_shape_std.ml
Properties	metaprl/refiner/term_shape_std.ml
Added	metaprl/refiner/term_shape_std.mli
Properties	metaprl/refiner/term_shape_std.mli
Added	metaprl/refiner/term_sig.ml
Properties	metaprl/refiner/term_sig.ml
+6 -3	metaprl/refiner/term_stable.ml
+4 -1	metaprl/refiner/term_stable.mli
Added	metaprl/refiner/term_std.ml
Properties	metaprl/refiner/term_std.ml
Added	metaprl/refiner/term_std.mli
Properties	metaprl/refiner/term_std.mli
Added	metaprl/refiner/term_subst_sig.ml
Properties	metaprl/refiner/term_subst_sig.ml
Added	metaprl/refiner/term_subst_std.ml
Properties	metaprl/refiner/term_subst_std.ml
Added	metaprl/refiner/term_subst_std.mli
Properties	metaprl/refiner/term_subst_std.mli
+8 -3	metaprl/refiner/term_table.ml
+5 -2	metaprl/refiner/term_table.mli
+6 -2	metaprl/refiner/term_template.ml
+4 -1	metaprl/refiner/term_template.mli
Deleted	metaprl/refiner/term_util.ml
Deleted	metaprl/refiner/term_util.mli
+6 -3	metaprl/refiner/theory.ml
+5 -2	metaprl/refiner/theory.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-05-27 09:50:05 -0700 (Wed, 27 May 1998)
Revision: 2185
Log message:

Fixed variable lists handling in alpha equality and unification

Changes	Path
+8 -4	metaprl/refiner/term_ds.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-05-27 11:55:12 -0700 (Wed, 27 May 1998)
Revision: 2186
Log message:

Removed simple_print_sig.mlz

Changes	Path
+0 -2	metaprl/refiner/Makefile

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-05-27 19:44:29 -0700 (Wed, 27 May 1998)
Revision: 2187
Log message:

Parameterized by the Term and TermSubst modules

Changes	Path
+9 -3	metaprl/refiner/term_meta_std.ml
+11 -3	metaprl/refiner/term_meta_std.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-05-27 19:45:13 -0700 (Wed, 27 May 1998)
Revision: 2188
Log message:

Parameterized TermMeta module with Term and TermSubst modules

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

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-05-27 19:53:12 -0700 (Wed, 27 May 1998)
Revision: 2189
Log message:

      Splitted Term_ds and Term_ds_simple modules into a smaller modules
      for use in the functorized refiner

Changes	Path
+8 -0	metaprl/refiner/Makefile
Added	metaprl/refiner/refiner_ds.ml
Properties	metaprl/refiner/refiner_ds.ml
Added	metaprl/refiner/refiner_ds.mli
Properties	metaprl/refiner/refiner_ds.mli
Added	metaprl/refiner/term_addr_ds.ml
Properties	metaprl/refiner/term_addr_ds.ml
Added	metaprl/refiner/term_addr_ds.mli
Properties	metaprl/refiner/term_addr_ds.mli
+361 -903	metaprl/refiner/term_ds.ml
+138 -198	metaprl/refiner/term_ds.mli
Deleted	metaprl/refiner/term_ds_simple.ml
Deleted	metaprl/refiner/term_ds_simple.mli
Added	metaprl/refiner/term_eval_ds.ml
Properties	metaprl/refiner/term_eval_ds.ml
Added	metaprl/refiner/term_eval_ds.mli
Properties	metaprl/refiner/term_eval_ds.mli
Added	metaprl/refiner/term_man_ds.ml
Properties	metaprl/refiner/term_man_ds.ml
Added	metaprl/refiner/term_man_ds.mli
Properties	metaprl/refiner/term_man_ds.mli
Added	metaprl/refiner/term_op_ds.ml
Properties	metaprl/refiner/term_op_ds.ml
Added	metaprl/refiner/term_op_ds.mli
Properties	metaprl/refiner/term_op_ds.mli
Added	metaprl/refiner/term_shape_ds.ml
Properties	metaprl/refiner/term_shape_ds.ml
Added	metaprl/refiner/term_shape_ds.mli
Properties	metaprl/refiner/term_shape_ds.mli
Added	metaprl/refiner/term_subst_ds.ml
Properties	metaprl/refiner/term_subst_ds.ml
Added	metaprl/refiner/term_subst_ds.mli
Properties	metaprl/refiner/term_subst_ds.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-05-28 06:48:44 -0700 (Thu, 28 May 1998)
Revision: 2190
Log message:

      Updated the editor to use new Refiner structure.
      ITT needs dform names.

Changes	Path
+4 -0	metaprl/Makefile
Properties	metaprl/editor/ml
+3 -0	metaprl/editor/ml/Makefile
Added	metaprl/editor/ml/io_proof.ml
Properties	metaprl/editor/ml/io_proof.ml
Added	metaprl/editor/ml/io_proof.mli
Properties	metaprl/editor/ml/io_proof.mli
Added	metaprl/editor/ml/io_proof_type.mlz
Properties	metaprl/editor/ml/io_proof_type.mlz
+10 -4	metaprl/editor/ml/package_df.ml
+7 -3	metaprl/editor/ml/package_df.mli
+337 -36	metaprl/editor/ml/package_info.ml
+16 -1	metaprl/editor/ml/package_info.mli
+21 -3	metaprl/editor/ml/package_type.mlz
+41 -35	metaprl/editor/ml/proof.ml
+10 -6	metaprl/editor/ml/proof.mli
+13 -4	metaprl/editor/ml/proof_edit.ml
+8 -4	metaprl/editor/ml/proof_edit.mli
+20 -15	metaprl/editor/ml/proof_step.ml
+10 -6	metaprl/editor/ml/proof_step.mli
+9 -7	metaprl/editor/ml/shell.ml
+5 -1	metaprl/editor/ml/shell.mli
+5 -1	metaprl/editor/ml/shell_null.ml
+6 -1	metaprl/editor/ml/shell_p4.ml
+5 -1	metaprl/editor/ml/shell_p4.mli
+118 -67	metaprl/editor/ml/shell_rewrite.ml
+12 -13	metaprl/editor/ml/shell_rewrite.mli
+7 -3	metaprl/editor/ml/shell_type.mlz
Properties	metaprl/filter
+0 -2	metaprl/filter/Makefile
+10 -6	metaprl/filter/filter_bin.ml
+22 -22	metaprl/filter/filter_cache.ml
+11 -6	metaprl/filter/filter_cache.mli
+10 -1	metaprl/filter/filter_cache_fun.ml
+7 -3	metaprl/filter/filter_parse.ml
+79 -26	metaprl/filter/filter_prog.ml
+12 -3	metaprl/filter/filter_prog.mli
Deleted	metaprl/filter/filter_proof.ml
Deleted	metaprl/filter/filter_proof.mli
Deleted	metaprl/filter/filter_proof_type.mlz
+20 -16	metaprl/filter/filter_summary.ml
+5 -1	metaprl/filter/filter_summary.mli
+5 -0	metaprl/library/ascii_scan.ml
+5 -0	metaprl/library/basic.ml
+5 -0	metaprl/library/bigInt.ml
+5 -0	metaprl/library/db.ml
+5 -0	metaprl/library/definition.ml
+5 -0	metaprl/library/int32.ml
+5 -0	metaprl/library/library.ml
+3 -0	metaprl/library/library_eval.ml
+9 -0	metaprl/library/library_type_base.ml
+5 -0	metaprl/library/link.ml
+5 -0	metaprl/library/mathBus.ml
+6 -2	metaprl/library/mbterm.ml
+5 -0	metaprl/library/nuprl5.ml
+5 -0	metaprl/library/object_id.ml
+5 -0	metaprl/library/oidtable.ml
+5 -0	metaprl/library/orb.ml
+7 -0	metaprl/library/registry.ml
+5 -0	metaprl/library/socketIo.ml
+5 -0	metaprl/library/tentfunctor.ml
+7 -2	metaprl/library/test.ml
+5 -0	metaprl/library/utils.ml
+3 -3	metaprl/mk/config
+2 -2	metaprl/refiner/Makefile
+8 -4	metaprl/theories/base/base_cache.ml
+8 -4	metaprl/theories/base/base_cache.mli
+7 -1	metaprl/theories/base/base_dform.ml
+32 -28	metaprl/theories/base/base_dtactic.ml
+5 -1	metaprl/theories/base/base_dtactic.mli
+4 -1	metaprl/theories/base/evaluator.ml
+1 -1	metaprl/theories/base/evaluator.mli
+30 -26	metaprl/theories/base/typeinf.ml
+14 -10	metaprl/theories/base/typeinf.mli
+1 -1	metaprl/theories/itt/Makefile
+5 -1	metaprl/theories/itt/itt_atom.ml
+5 -1	metaprl/theories/itt/itt_atom.mli
+5 -1	metaprl/theories/itt/itt_dfun.ml
+5 -1	metaprl/theories/itt/itt_dfun.mli
+5 -1	metaprl/theories/itt/itt_dprod.ml
+5 -1	metaprl/theories/itt/itt_dprod.mli
+5 -1	metaprl/theories/itt/itt_equal.ml
+5 -1	metaprl/theories/itt/itt_equal.mli
+5 -1	metaprl/theories/itt/itt_ext_equal.ml
+5 -1	metaprl/theories/itt/itt_ext_equal.mli
+5 -1	metaprl/theories/itt/itt_fun.ml
+5 -1	metaprl/theories/itt/itt_int.ml
+5 -1	metaprl/theories/itt/itt_int.mli
+5 -1	metaprl/theories/itt/itt_isect.ml
+5 -1	metaprl/theories/itt/itt_isect.mli
+5 -1	metaprl/theories/itt/itt_list.ml
+5 -1	metaprl/theories/itt/itt_list.mli
+5 -1	metaprl/theories/itt/itt_logic.ml
+5 -1	metaprl/theories/itt/itt_logic.mli
+5 -1	metaprl/theories/itt/itt_prec.ml
+5 -1	metaprl/theories/itt/itt_prec.mli
+5 -1	metaprl/theories/itt/itt_prod.ml
+5 -1	metaprl/theories/itt/itt_quotient.ml
+5 -1	metaprl/theories/itt/itt_quotient.mli
+1 -1	metaprl/theories/itt/itt_redrules.ml
+5 -1	metaprl/theories/itt/itt_rfun.ml
+5 -1	metaprl/theories/itt/itt_rfun.mli
+5 -1	metaprl/theories/itt/itt_set.ml
+5 -1	metaprl/theories/itt/itt_set.mli
+5 -1	metaprl/theories/itt/itt_soft.ml
+5 -1	metaprl/theories/itt/itt_soft.mli
+21 -17	metaprl/theories/itt/itt_squash.ml
+5 -1	metaprl/theories/itt/itt_squash.mli
+5 -1	metaprl/theories/itt/itt_srec.ml
+5 -1	metaprl/theories/itt/itt_srec.mli
+5 -1	metaprl/theories/itt/itt_struct.ml
+5 -1	metaprl/theories/itt/itt_struct.mli
+5 -1	metaprl/theories/itt/itt_subtype.ml
+5 -1	metaprl/theories/itt/itt_subtype.mli
+5 -1	metaprl/theories/itt/itt_union.ml
+5 -1	metaprl/theories/itt/itt_union.mli
+5 -1	metaprl/theories/itt/itt_unit.ml
+5 -1	metaprl/theories/itt/itt_unit.mli
+5 -1	metaprl/theories/itt/itt_void.ml
+5 -1	metaprl/theories/itt/itt_void.mli
+5 -0	metaprl/theories/ocaml/ocaml_base_df.ml
+5 -0	metaprl/theories/ocaml/perv.ml
+5 -1	metaprl/theories/rewrite/rw_beta.ml
+5 -1	metaprl/theories/tactic/options.ml
+35 -29	metaprl/theories/tactic/sequent.ml
+5 -1	metaprl/theories/tactic/sequent.mli
+7 -2	metaprl/theories/tactic/tactic_cache.ml
+5 -1	metaprl/theories/tactic/tactic_cache.mli
+23 -8	metaprl/theories/tactic/tactic_type.mlz
+14 -9	metaprl/theories/tactic/tacticals.ml
+5 -1	metaprl/theories/tactic/tacticals.mli
+1 -0	metaprl/util/Makefile

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-05-28 08:02:46 -0700 (Thu, 28 May 1998)
Revision: 2191
Log message:

Partitioned refiner into subdirectories.

Changes	Path
+9 -1	metaprl/filter/Makefile
+5 -1	metaprl/library/Makefile
Properties	metaprl/refiner
Deleted	metaprl/refiner/.cprc
+29 -75	metaprl/refiner/Makefile
Deleted	metaprl/refiner/dform.ml
Deleted	metaprl/refiner/dform.mli
Deleted	metaprl/refiner/dform_print.ml
Deleted	metaprl/refiner/dform_print.mli
Deleted	metaprl/refiner/ml_file.ml
Deleted	metaprl/refiner/ml_file.mli
Deleted	metaprl/refiner/ml_format.mli
Deleted	metaprl/refiner/ml_format_sig.ml
Deleted	metaprl/refiner/ml_print.ml
Deleted	metaprl/refiner/ml_print.mli
Deleted	metaprl/refiner/ml_print_sig.ml
Deleted	metaprl/refiner/ml_string.ml
Deleted	metaprl/refiner/ml_string.mli
Deleted	metaprl/refiner/opname.ml
Deleted	metaprl/refiner/opname.mli
Properties	metaprl/refiner/refbase
Added	metaprl/refiner/refbase/Makefile
Properties	metaprl/refiner/refbase/Makefile
Added	metaprl/refiner/refbase/opname.ml
Properties	metaprl/refiner/refbase/opname.ml
Added	metaprl/refiner/refbase/opname.mli
Properties	metaprl/refiner/refbase/opname.mli
Deleted	metaprl/refiner/refine.ml
Deleted	metaprl/refiner/refine.mli
Deleted	metaprl/refiner/refine_exn.ml
Deleted	metaprl/refiner/refine_exn.mli
Deleted	metaprl/refiner/refine_sig.ml
Properties	metaprl/refiner/refiner
Added	metaprl/refiner/refiner/Makefile
Properties	metaprl/refiner/refiner/Makefile
Added	metaprl/refiner/refiner/refine.ml
Properties	metaprl/refiner/refiner/refine.ml
Added	metaprl/refiner/refiner/refine.mli
Properties	metaprl/refiner/refiner/refine.mli
Added	metaprl/refiner/refiner/refiner.ml
Properties	metaprl/refiner/refiner/refiner.ml
Added	metaprl/refiner/refiner/refiner.mli
Properties	metaprl/refiner/refiner/refiner.mli
Added	metaprl/refiner/refiner/refiner_ds.ml
Properties	metaprl/refiner/refiner/refiner_ds.ml
Added	metaprl/refiner/refiner/refiner_ds.mli
Properties	metaprl/refiner/refiner/refiner_ds.mli
Added	metaprl/refiner/refiner/refiner_std.ml
Properties	metaprl/refiner/refiner/refiner_std.ml
Added	metaprl/refiner/refiner/refiner_std.mli
Properties	metaprl/refiner/refiner/refiner_std.mli
Added	metaprl/refiner/refiner/rewrite.ml
Properties	metaprl/refiner/refiner/rewrite.ml
Added	metaprl/refiner/refiner/rewrite.mli
Properties	metaprl/refiner/refiner/rewrite.mli
Deleted	metaprl/refiner/refiner.ml
Deleted	metaprl/refiner/refiner.mli
Deleted	metaprl/refiner/refiner_ds.ml
Deleted	metaprl/refiner/refiner_ds.mli
Deleted	metaprl/refiner/refiner_sig.ml
Deleted	metaprl/refiner/refiner_std.ml
Deleted	metaprl/refiner/refiner_std.mli
Properties	metaprl/refiner/reflib
Added	metaprl/refiner/reflib/Makefile
Properties	metaprl/refiner/reflib/Makefile
Added	metaprl/refiner/reflib/dform.ml
Properties	metaprl/refiner/reflib/dform.ml
Added	metaprl/refiner/reflib/dform.mli
Properties	metaprl/refiner/reflib/dform.mli
Added	metaprl/refiner/reflib/dform_print.ml
Properties	metaprl/refiner/reflib/dform_print.ml
Added	metaprl/refiner/reflib/dform_print.mli
Properties	metaprl/refiner/reflib/dform_print.mli
Added	metaprl/refiner/reflib/ml_file.ml
Properties	metaprl/refiner/reflib/ml_file.ml
Added	metaprl/refiner/reflib/ml_file.mli
Properties	metaprl/refiner/reflib/ml_file.mli
Added	metaprl/refiner/reflib/ml_format.ml
Properties	metaprl/refiner/reflib/ml_format.ml
Added	metaprl/refiner/reflib/ml_format.mli
Properties	metaprl/refiner/reflib/ml_format.mli
Added	metaprl/refiner/reflib/ml_format_sig.mlz
Properties	metaprl/refiner/reflib/ml_format_sig.mlz
Added	metaprl/refiner/reflib/ml_print.ml
Properties	metaprl/refiner/reflib/ml_print.ml
Added	metaprl/refiner/reflib/ml_print.mli
Properties	metaprl/refiner/reflib/ml_print.mli
Added	metaprl/refiner/reflib/ml_print_sig.mlz
Properties	metaprl/refiner/reflib/ml_print_sig.mlz
Added	metaprl/refiner/reflib/ml_string.ml
Properties	metaprl/refiner/reflib/ml_string.ml
Added	metaprl/refiner/reflib/ml_string.mli
Properties	metaprl/refiner/reflib/ml_string.mli
Added	metaprl/refiner/reflib/refine_exn.ml
Properties	metaprl/refiner/reflib/refine_exn.ml
Added	metaprl/refiner/reflib/refine_exn.mli
Properties	metaprl/refiner/reflib/refine_exn.mli
Added	metaprl/refiner/reflib/resource.ml
Properties	metaprl/refiner/reflib/resource.ml
Added	metaprl/refiner/reflib/resource.mli
Properties	metaprl/refiner/reflib/resource.mli
Added	metaprl/refiner/reflib/rformat.ml
Properties	metaprl/refiner/reflib/rformat.ml
Added	metaprl/refiner/reflib/rformat.mli
Properties	metaprl/refiner/reflib/rformat.mli
Added	metaprl/refiner/reflib/simple_print.ml
Properties	metaprl/refiner/reflib/simple_print.ml
Added	metaprl/refiner/reflib/simple_print.mli
Properties	metaprl/refiner/reflib/simple_print.mli
Added	metaprl/refiner/reflib/term_dtable.ml
Properties	metaprl/refiner/reflib/term_dtable.ml
Added	metaprl/refiner/reflib/term_dtable.mli
Properties	metaprl/refiner/reflib/term_dtable.mli
Added	metaprl/refiner/reflib/term_stable.ml
Properties	metaprl/refiner/reflib/term_stable.ml
Added	metaprl/refiner/reflib/term_stable.mli
Properties	metaprl/refiner/reflib/term_stable.mli
Added	metaprl/refiner/reflib/term_table.ml
Properties	metaprl/refiner/reflib/term_table.ml
Added	metaprl/refiner/reflib/term_table.mli
Properties	metaprl/refiner/reflib/term_table.mli
Added	metaprl/refiner/reflib/term_template.ml
Properties	metaprl/refiner/reflib/term_template.ml
Added	metaprl/refiner/reflib/term_template.mli
Properties	metaprl/refiner/reflib/term_template.mli
Added	metaprl/refiner/reflib/theory.ml
Properties	metaprl/refiner/reflib/theory.ml
Added	metaprl/refiner/reflib/theory.mli
Properties	metaprl/refiner/reflib/theory.mli
Properties	metaprl/refiner/refsig
Added	metaprl/refiner/refsig/Makefile
Properties	metaprl/refiner/refsig/Makefile
Added	metaprl/refiner/refsig/refine_sig.ml
Properties	metaprl/refiner/refsig/refine_sig.ml
Added	metaprl/refiner/refsig/refiner_sig.ml
Properties	metaprl/refiner/refsig/refiner_sig.ml
Added	metaprl/refiner/refsig/resource.mlz
Properties	metaprl/refiner/refsig/resource.mlz
Added	metaprl/refiner/refsig/rewrite_sig.ml
Properties	metaprl/refiner/refsig/rewrite_sig.ml
Added	metaprl/refiner/refsig/term_addr_sig.ml
Properties	metaprl/refiner/refsig/term_addr_sig.ml
Added	metaprl/refiner/refsig/term_eval_sig.ml
Properties	metaprl/refiner/refsig/term_eval_sig.ml
Added	metaprl/refiner/refsig/term_man_sig.ml
Properties	metaprl/refiner/refsig/term_man_sig.ml
Added	metaprl/refiner/refsig/term_meta_sig.ml
Properties	metaprl/refiner/refsig/term_meta_sig.ml
Added	metaprl/refiner/refsig/term_op_sig.ml
Properties	metaprl/refiner/refsig/term_op_sig.ml
Added	metaprl/refiner/refsig/term_shape_sig.ml
Properties	metaprl/refiner/refsig/term_shape_sig.ml
Added	metaprl/refiner/refsig/term_sig.ml
Properties	metaprl/refiner/refsig/term_sig.ml
Added	metaprl/refiner/refsig/term_subst_sig.ml
Properties	metaprl/refiner/refsig/term_subst_sig.ml
Deleted	metaprl/refiner/resource.ml
Deleted	metaprl/refiner/rewrite.ml
Deleted	metaprl/refiner/rewrite.mli
Deleted	metaprl/refiner/rewrite_sig.ml
Deleted	metaprl/refiner/rformat.ml
Deleted	metaprl/refiner/rformat.mli
Deleted	metaprl/refiner/simple_print.ml
Deleted	metaprl/refiner/simple_print.mli
Deleted	metaprl/refiner/term_addr_ds.ml
Deleted	metaprl/refiner/term_addr_ds.mli
Deleted	metaprl/refiner/term_addr_sig.ml
Deleted	metaprl/refiner/term_addr_std.ml
Deleted	metaprl/refiner/term_addr_std.mli
Properties	metaprl/refiner/term_ds
Added	metaprl/refiner/term_ds/Makefile
Properties	metaprl/refiner/term_ds/Makefile
Added	metaprl/refiner/term_ds/term_addr_ds.ml
Properties	metaprl/refiner/term_ds/term_addr_ds.ml
Added	metaprl/refiner/term_ds/term_addr_ds.mli
Properties	metaprl/refiner/term_ds/term_addr_ds.mli
Added	metaprl/refiner/term_ds/term_ds.ml
Properties	metaprl/refiner/term_ds/term_ds.ml
Added	metaprl/refiner/term_ds/term_ds.mli
Properties	metaprl/refiner/term_ds/term_ds.mli
Added	metaprl/refiner/term_ds/term_eval_ds.ml
Properties	metaprl/refiner/term_ds/term_eval_ds.ml
Added	metaprl/refiner/term_ds/term_eval_ds.mli
Properties	metaprl/refiner/term_ds/term_eval_ds.mli
Added	metaprl/refiner/term_ds/term_man_ds.ml
Properties	metaprl/refiner/term_ds/term_man_ds.ml
Added	metaprl/refiner/term_ds/term_man_ds.mli
Properties	metaprl/refiner/term_ds/term_man_ds.mli
Added	metaprl/refiner/term_ds/term_op_ds.ml
Properties	metaprl/refiner/term_ds/term_op_ds.ml
Added	metaprl/refiner/term_ds/term_op_ds.mli
Properties	metaprl/refiner/term_ds/term_op_ds.mli
Added	metaprl/refiner/term_ds/term_shape_ds.ml
Properties	metaprl/refiner/term_ds/term_shape_ds.ml
Added	metaprl/refiner/term_ds/term_shape_ds.mli
Properties	metaprl/refiner/term_ds/term_shape_ds.mli
Added	metaprl/refiner/term_ds/term_subst_ds.ml
Properties	metaprl/refiner/term_ds/term_subst_ds.ml
Added	metaprl/refiner/term_ds/term_subst_ds.mli
Properties	metaprl/refiner/term_ds/term_subst_ds.mli
Deleted	metaprl/refiner/term_ds.ml
Deleted	metaprl/refiner/term_ds.mli
Deleted	metaprl/refiner/term_dtable.ml
Deleted	metaprl/refiner/term_dtable.mli
Deleted	metaprl/refiner/term_eval_ds.ml
Deleted	metaprl/refiner/term_eval_ds.mli
Deleted	metaprl/refiner/term_eval_sig.ml
Deleted	metaprl/refiner/term_eval_std.ml
Deleted	metaprl/refiner/term_eval_std.mli
Deleted	metaprl/refiner/term_man_ds.ml
Deleted	metaprl/refiner/term_man_ds.mli
Deleted	metaprl/refiner/term_man_sig.ml
Deleted	metaprl/refiner/term_man_std.ml
Deleted	metaprl/refiner/term_man_std.mli
Deleted	metaprl/refiner/term_meta_sig.ml
Deleted	metaprl/refiner/term_meta_std.ml
Deleted	metaprl/refiner/term_meta_std.mli
Deleted	metaprl/refiner/term_op_ds.ml
Deleted	metaprl/refiner/term_op_ds.mli
Deleted	metaprl/refiner/term_op_sig.ml
Deleted	metaprl/refiner/term_op_std.ml
Deleted	metaprl/refiner/term_op_std.mli
Deleted	metaprl/refiner/term_shape_ds.ml
Deleted	metaprl/refiner/term_shape_ds.mli
Deleted	metaprl/refiner/term_shape_sig.ml
Deleted	metaprl/refiner/term_shape_std.ml
Deleted	metaprl/refiner/term_shape_std.mli
Deleted	metaprl/refiner/term_sig.ml
Deleted	metaprl/refiner/term_stable.ml
Deleted	metaprl/refiner/term_stable.mli
Properties	metaprl/refiner/term_std
Added	metaprl/refiner/term_std/Makefile
Properties	metaprl/refiner/term_std/Makefile
Added	metaprl/refiner/term_std/term_addr_std.ml
Properties	metaprl/refiner/term_std/term_addr_std.ml
Added	metaprl/refiner/term_std/term_addr_std.mli
Properties	metaprl/refiner/term_std/term_addr_std.mli
Added	metaprl/refiner/term_std/term_eval_std.ml
Properties	metaprl/refiner/term_std/term_eval_std.ml
Added	metaprl/refiner/term_std/term_eval_std.mli
Properties	metaprl/refiner/term_std/term_eval_std.mli
Added	metaprl/refiner/term_std/term_man_std.ml
Properties	metaprl/refiner/term_std/term_man_std.ml
Added	metaprl/refiner/term_std/term_man_std.mli
Properties	metaprl/refiner/term_std/term_man_std.mli
Added	metaprl/refiner/term_std/term_meta_std.ml
Properties	metaprl/refiner/term_std/term_meta_std.ml
Added	metaprl/refiner/term_std/term_meta_std.mli
Properties	metaprl/refiner/term_std/term_meta_std.mli
Added	metaprl/refiner/term_std/term_op_std.ml
Properties	metaprl/refiner/term_std/term_op_std.ml
Added	metaprl/refiner/term_std/term_op_std.mli
Properties	metaprl/refiner/term_std/term_op_std.mli
Added	metaprl/refiner/term_std/term_shape_std.ml
Properties	metaprl/refiner/term_std/term_shape_std.ml
Added	metaprl/refiner/term_std/term_shape_std.mli
Properties	metaprl/refiner/term_std/term_shape_std.mli
Added	metaprl/refiner/term_std/term_std.ml
Properties	metaprl/refiner/term_std/term_std.ml
Added	metaprl/refiner/term_std/term_std.mli
Properties	metaprl/refiner/term_std/term_std.mli
Added	metaprl/refiner/term_std/term_subst_std.ml
Properties	metaprl/refiner/term_std/term_subst_std.ml
Added	metaprl/refiner/term_std/term_subst_std.mli
Properties	metaprl/refiner/term_std/term_subst_std.mli
Deleted	metaprl/refiner/term_std.ml
Deleted	metaprl/refiner/term_std.mli
Deleted	metaprl/refiner/term_subst_ds.ml
Deleted	metaprl/refiner/term_subst_ds.mli
Deleted	metaprl/refiner/term_subst_sig.ml
Deleted	metaprl/refiner/term_subst_std.ml
Deleted	metaprl/refiner/term_subst_std.mli
Deleted	metaprl/refiner/term_table.ml
Deleted	metaprl/refiner/term_table.mli
Deleted	metaprl/refiner/term_template.ml
Deleted	metaprl/refiner/term_template.mli
Deleted	metaprl/refiner/theory.ml
Deleted	metaprl/refiner/theory.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-05-28 13:34:47 -0700 (Thu, 28 May 1998)
Revision: 2192
Log message:

Use cp -pf for copying %.mlz -> %.ml & %.mli

Changes	Path
+3 -2	metaprl/mk/config

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-05-28 15:10:02 -0700 (Thu, 28 May 1998)
Revision: 2193
Log message:

Updated Makefiles.

Changes	Path
+73 -10	metaprl/refiner/Makefile
+13 -8	metaprl/refiner/refbase/Makefile
+15 -12	metaprl/refiner/refiner/Makefile
+17 -25	metaprl/refiner/reflib/Makefile
Deleted	metaprl/refiner/reflib/resource.ml
Deleted	metaprl/refiner/reflib/resource.mli
Added	metaprl/refiner/reflib/resource.mlz
Properties	metaprl/refiner/reflib/resource.mlz
+16 -19	metaprl/refiner/refsig/Makefile
+16 -15	metaprl/refiner/term_ds/Makefile
+16 -16	metaprl/refiner/term_std/Makefile

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-05-28 15:59:33 -0700 (Thu, 28 May 1998)
Revision: 2194
Log message:

Command to run Nuprl-Light.

Changes	Path
Added	metaprl/editor/ml/nl
Properties	metaprl/editor/ml/nl

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-05-28 17:42:17 -0700 (Thu, 28 May 1998)
Revision: 2195
Log message:

File listings.

Changes	Path
Added	metaprl/refiner/refbase/Files
Properties	metaprl/refiner/refbase/Files
Added	metaprl/refiner/refiner/Files
Properties	metaprl/refiner/refiner/Files
Added	metaprl/refiner/reflib/Files
Properties	metaprl/refiner/reflib/Files
Added	metaprl/refiner/refsig/Files
Properties	metaprl/refiner/refsig/Files
Added	metaprl/refiner/term_ds/Files
Properties	metaprl/refiner/term_ds/Files
Added	metaprl/refiner/term_std/Files
Properties	metaprl/refiner/term_std/Files
+1 -1	metaprl/refiner/term_std/Makefile

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-05-28 18:19:37 -0700 (Thu, 28 May 1998)
Revision: 2196
Log message:

*** empty log message ***

Changes	Path
Properties	metaprl/refiner/reflib

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-05-28 18:56:08 -0700 (Thu, 28 May 1998)
Revision: 2197
Log message:

Added time_it function

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

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-05-28 19:29:21 -0700 (Thu, 28 May 1998)
Revision: 2198
Log message:

      Created refiner/term_gen directory
      Moved renamed term_std/term_meta_std to term_gen/term_meta_gen

Changes	Path
+8 -0	metaprl/refiner/Makefile
+1 -1	metaprl/refiner/refiner/Makefile
+5 -1	metaprl/refiner/refiner/refiner_ds.ml
+5 -1	metaprl/refiner/refiner/refiner_std.ml
Properties	metaprl/refiner/term_gen
Added	metaprl/refiner/term_gen/Files
Properties	metaprl/refiner/term_gen/Files
Added	metaprl/refiner/term_gen/Makefile
Properties	metaprl/refiner/term_gen/Makefile
Added	metaprl/refiner/term_gen/term_meta_gen.ml
Properties	metaprl/refiner/term_gen/term_meta_gen.ml
Added	metaprl/refiner/term_gen/term_meta_gen.mli
Properties	metaprl/refiner/term_gen/term_meta_gen.mli
+0 -1	metaprl/refiner/term_std/Files
Deleted	metaprl/refiner/term_std/term_meta_std.ml
Deleted	metaprl/refiner/term_std/term_meta_std.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-05-28 21:11:05 -0700 (Thu, 28 May 1998)
Revision: 2199
Log message:

      Fixed some typos.
      Use == instead of = for comparing opnames.

Changes	Path
+8 -4	metaprl/refiner/term_std/term_man_std.ml
+33 -29	metaprl/refiner/term_std/term_op_std.ml
+5 -1	metaprl/refiner/term_std/term_subst_std.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-05-28 21:22:13 -0700 (Thu, 28 May 1998)
Revision: 2200
Log message:

Fixed a typo

Changes	Path
+1 -1	metaprl/refiner/Makefile

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-05-29 07:53:34 -0700 (Fri, 29 May 1998)
Revision: 2201
Log message:

Better Makefiles.

Changes	Path
+6 -18	metaprl/Makefile
Properties	metaprl/bin
Added	metaprl/bin/Makefile
Properties	metaprl/bin/Makefile
+12 -2	metaprl/clib/Makefile
+36 -33	metaprl/editor/emacs/caml.el
+28 -21	metaprl/editor/ml/Makefile
+9 -0	metaprl/editor/ml/package_info.ml
+4 -0	metaprl/editor/ml/package_type.mlz
+63 -0	metaprl/editor/ml/shell.ml
+23 -9	metaprl/editor/ml/shell_rewrite.ml
+5 -8	metaprl/editor/ml/shell_rewrite.mli
+119 -23	metaprl/filter/Makefile
+4 -0	metaprl/filter/filter_cache_fun.ml
+4 -1	metaprl/filter/filter_summary.ml
+4 -1	metaprl/filter/filter_summary.mli
+4 -0	metaprl/filter/filter_summary_type.mlz
+3 -7	metaprl/filter/infix.ml
+30 -21	metaprl/filter/prlcomp.ml
+1 -0	metaprl/horus/Makefile
Properties	metaprl/lib
Added	metaprl/lib/Makefile
Properties	metaprl/lib/Makefile
+21 -15	metaprl/library/Makefile
+33 -17	metaprl/mk/config
+15 -6	metaprl/mllib/Makefile
+3 -2	metaprl/theories/base/Makefile
+3 -2	metaprl/theories/itt/Makefile
+1 -0	metaprl/theories/lf/Makefile
+4 -2	metaprl/theories/ocaml/Makefile
+2 -1	metaprl/theories/ocaml_sos/Makefile
+4 -3	metaprl/theories/tactic/Makefile
+2 -4	metaprl/util/Makefile
+1 -3	metaprl/util/ocamldep.mll

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-05-29 13:51:12 -0700 (Fri, 29 May 1998)
Revision: 2202
Log message:

Need to update ocamldep.

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

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-05-29 14:12:31 -0700 (Fri, 29 May 1998)
Revision: 2203
Log message:

Need to update ocamldep.

Changes	Path
+4 -1	metaprl/filter/prlcomp.ml
+0 -1	metaprl/theories/ocaml/Makefile

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-05-29 17:58:33 -0700 (Fri, 29 May 1998)
Revision: 2204
Log message:

Added -I ../../library

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

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-05-30 10:15:28 -0700 (Sat, 30 May 1998)
Revision: 2205
Log message:

infix.ml is generated from infix.pre.ml and it should not be in the cvs repository

Changes	Path
Deleted	metaprl/filter/infix.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-05-30 11:31:19 -0700 (Sat, 30 May 1998)
Revision: 2206
Log message:

Fixed the style - placed |'s in the beginning of the lines.

Changes	Path
+22 -22	metaprl/refiner/term_ds/term_ds.ml
+4 -4	metaprl/refiner/term_ds/term_ds.mli
+8 -8	metaprl/refiner/term_ds/term_subst_ds.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-05-30 12:18:49 -0700 (Sat, 30 May 1998)
Revision: 2207
Log message:

Eliminated white space in empty lines.

Changes	Path
+0 -10	metaprl/refiner/term_ds/term_addr_ds.ml
+0 -8	metaprl/refiner/term_ds/term_ds.ml
+0 -3	metaprl/refiner/term_ds/term_ds.mli
+0 -83	metaprl/refiner/term_ds/term_op_ds.ml
+0 -4	metaprl/refiner/term_ds/term_shape_ds.ml
+0 -22	metaprl/refiner/term_ds/term_subst_ds.ml
+3 -12	metaprl/refiner/term_std/term_addr_std.ml
+3 -1	metaprl/refiner/term_std/term_eval_std.ml
+3 -38	metaprl/refiner/term_std/term_man_std.ml
+3 -79	metaprl/refiner/term_std/term_op_std.ml
+3 -4	metaprl/refiner/term_std/term_shape_std.ml
+3 -53	metaprl/refiner/term_std/term_std.ml
+3 -12	metaprl/refiner/term_std/term_std.mli
+3 -44	metaprl/refiner/term_std/term_subst_std.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-05-30 14:13:59 -0700 (Sat, 30 May 1998)
Revision: 2208
Log message:

infix.ml is generated from infix.pre.ml and it should not be in the cvs repository

Changes	Path
Properties	metaprl/filter