Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-10-07 11:18:44 -0700 (Thu, 07 Oct 1999)
Revision: 2815
Log message:

      - Added link to MetaPRL-related seminars page
      - Some pages had "NLOverview" instead of "MPOverview" - fixed
      

Changes  Path
+1 -1 metaprl/doc/htmlman/default.html
+2 -1 metaprl/doc/htmlman/framework/mp-index.html
+1 -0 metaprl/doc/htmlman/mp-index.html
+1 -0 metaprl/doc/htmlman/mp.html
Added metaprl/doc/htmlman/seminars.html
Properties metaprl/doc/htmlman/seminars.html
+1 -0 metaprl/doc/htmlman/system/mp-index.html
+1 -1 metaprl/doc/htmlman/tutorial/mp-index.html
+2 -1 metaprl/doc/htmlman/user-guide/mp-index.html

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-10-08 15:38:35 -0700 (Fri, 08 Oct 1999)
Revision: 2816
Log message:

      - Updated several bug descriptions
      - Numbered all bugs so that we can easier refer to them
      - I suggest that we start all bug descriptions by
      i.j) (Added on <date> by <login>. Confirmed on <date> by <login> ...)
      So that we know how old the bug is and when was the last time we actually saw the bug.
      This should help us to determine which bugs may be already gone and which bugs
      are around too long and need to be finally fixed
      

Changes  Path
+46 -63 metaprl/BUGS

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-10-16 13:21:52 -0700 (Sat, 16 Oct 1999)
Revision: 2817
Log message:

      Changed alpha_equal_* in Term_ds and Term_std to be consistent with Nuprl:
      Now bound terms x,x.'x and y,x.'x are considered alpha equal while
      x,x.'x and x,y.'x are not.
      

Changes  Path
+0 -1 metaprl/editor/ml/x.ml
+11 -5 metaprl/mllib/list_util.ml
+1 -0 metaprl/mllib/list_util.mli
+1 -1 metaprl/refiner/refsig/term_subst_sig.ml
+2 -2 metaprl/refiner/term_ds/term_subst_ds.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-10-16 14:28:15 -0700 (Sat, 16 Oct 1999)
Revision: 2818
Log message:

      Updated the bug list:
      - The bug (3.4) is fixed (see my previous commit).
      - Added more information on several other bugs.
      

Changes  Path
+14 -8 metaprl/BUGS

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-10-21 10:29:30 -0700 (Thu, 21 Oct 1999)
Revision: 2819
Log message:

      There was a small typo in a sub_resource.
      Thanks to Carl R. Witty <cwitty@newtonlabs.com> for finding it!
      I am sorry it took so long to fix it - I completely forgot about it.
      

Changes  Path
+1 -1 metaprl/theories/itt/itt_dprod.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-10-21 12:25:39 -0700 (Thu, 21 Oct 1999)
Revision: 2820
Log message:

      This is no longer used. set_sig.mlz is used instead
      

Changes  Path
Deleted metaprl/mllib/mp_set.mlz

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-10-21 16:32:11 -0700 (Thu, 21 Oct 1999)
Revision: 2821
Log message:

      I wrote a short description of some of the useful modules we have here:
      sets, linear sets and tables.
      
      I would be nice to try to extend this documentation and keep it up-to-date.
      
      I am planning to submit a links to this file (http://ensemble01.cs.cornell.edu:12000/cvsweb/~checkout~/meta-prl/mllib/index.html )
      to several OCaml code indexes:
      http://caml.inria.fr/hump.html
      http://miss.wu-wien.ac.at/~mottl/ocaml_sources/intro.html
      

Changes  Path
Added metaprl/mllib/index.html
Properties metaprl/mllib/index.html

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-10-21 18:07:59 -0700 (Thu, 21 Oct 1999)
Revision: 2822
Log message:

      Added new function to mp_debug
      let show_loading s = if !debug_load then Printf.eprintf s eflush
      
      and replaced all usages of debug_load with show_loading
      

Changes  Path
+1 -2 metaprl/editor/ml/io_proof.ml
+1 -2 metaprl/editor/ml/library_eval.ml
+1 -2 metaprl/editor/ml/library_test.ml
+3 -6 metaprl/editor/ml/mp_top.ml
+1 -2 metaprl/editor/ml/package_df.ml
+1 -2 metaprl/editor/ml/package_edit.ml
+1 -2 metaprl/editor/ml/package_info.ml
+1 -2 metaprl/editor/ml/package_int.ml
+1 -2 metaprl/editor/ml/proof_edit.ml
+1 -2 metaprl/editor/ml/proof_step.ml
+2 -4 metaprl/editor/ml/shell.ml
+1 -2 metaprl/editor/ml/shell_http.ml
+1 -2 metaprl/editor/ml/shell_mp.ml
+1 -2 metaprl/editor/ml/shell_rewrite.ml
+1 -2 metaprl/editor/ml/shell_rule.ml
+1 -2 metaprl/evaluator/evaluator.ml
+1 -2 metaprl/evaluator/itt_redrules.ml
+1 -2 metaprl/filter/base/filter_ast.ml
+1 -2 metaprl/filter/base/filter_buffer.ml
+1 -2 metaprl/filter/base/filter_cache.ml
+1 -2 metaprl/filter/base/filter_cache_fun.ml
+1 -2 metaprl/filter/base/filter_comment.ml
+1 -2 metaprl/filter/base/filter_grammar.ml
+1 -2 metaprl/filter/base/filter_hash.ml
+1 -2 metaprl/filter/base/filter_html.ml
+1 -2 metaprl/filter/base/filter_ocaml.ml
+5 -11 metaprl/filter/base/filter_prog.ml
+1 -2 metaprl/filter/base/filter_summary.ml
+1 -2 metaprl/filter/base/filter_summary_io.ml
+1 -2 metaprl/filter/base/filter_summary_util.ml
+1 -2 metaprl/filter/base/filter_util.ml
+1 -2 metaprl/filter/base/free_vars.ml
+1 -2 metaprl/filter/base/mLast_util.ml
+1 -2 metaprl/filter/base/term_grammar.ml
+1 -2 metaprl/filter/boot/conversionals_boot.ml
+1 -2 metaprl/filter/boot/proof_boot.ml
+1 -2 metaprl/filter/boot/sequent_boot.ml
+1 -2 metaprl/filter/boot/tactic_boot.ml
+1 -2 metaprl/filter/boot/tacticals_boot.ml
+1 -2 metaprl/filter/filter/filter_bin.ml
+1 -2 metaprl/filter/filter/filter_convert.ml
+1 -2 metaprl/filter/filter/filter_main.ml
+1 -2 metaprl/filter/filter/filter_parse.ml
+1 -2 metaprl/filter/filter/prlcomp.ml
+1 -2 metaprl/library/ascii_scan.ml
+2 -3 metaprl/library/basic.ml
+1 -2 metaprl/library/bigInt.ml
+1 -2 metaprl/library/db.ml
+1 -2 metaprl/library/definition.ml
+1 -2 metaprl/library/int32.ml
+1 -2 metaprl/library/library.ml
+1 -2 metaprl/library/library_type_base.ml
+1 -2 metaprl/library/link.ml
+1 -2 metaprl/library/mathBus.ml
+1 -2 metaprl/library/mbterm.ml
+1 -2 metaprl/library/nuprl5.ml
+1 -2 metaprl/library/object_id.ml
+1 -2 metaprl/library/oidtable.ml
+1 -2 metaprl/library/orb.ml
+1 -2 metaprl/library/registry.ml
+1 -2 metaprl/library/socketIo.ml
+1 -2 metaprl/library/tentfunctor.ml
+1 -2 metaprl/library/test.ml
+1 -2 metaprl/library/utils.ml
+1 -2 metaprl/mllib/array_util.ml
+1 -2 metaprl/mllib/bitset.ml
+1 -2 metaprl/mllib/env_arg.ml
+1 -2 metaprl/mllib/file_base.ml
+1 -2 metaprl/mllib/file_type_base.ml
+1 -2 metaprl/mllib/file_util.ml
+1 -2 metaprl/mllib/filename_util.ml
+1 -2 metaprl/mllib/imp_dag.ml
+1 -2 metaprl/mllib/list_util.ml
+1 -2 metaprl/mllib/mp_ctype.ml
+1 -0 metaprl/mllib/mp_debug.ml
+2 -4 metaprl/mllib/mp_debug.mli
+1 -2 metaprl/mllib/precedence.ml
+1 -2 metaprl/mllib/ref_util.ml
+1 -2 metaprl/mllib/string_util.ml
+1 -2 metaprl/refiner/refbase/opname.ml
+1 -2 metaprl/refiner/refiner/refine.ml
+1 -2 metaprl/refiner/reflib/dform.ml
+1 -2 metaprl/refiner/reflib/dform_print.ml
+1 -2 metaprl/refiner/reflib/ml_file.ml
+1 -2 metaprl/refiner/reflib/ml_format.ml
+1 -2 metaprl/refiner/reflib/ml_print.ml
+1 -2 metaprl/refiner/reflib/ml_string.ml
+1 -2 metaprl/refiner/reflib/mp_resource.ml
+1 -2 metaprl/refiner/reflib/refine_exn.ml
+1 -2 metaprl/refiner/reflib/rformat.ml
+1 -2 metaprl/refiner/reflib/simple_print.ml
+1 -2 metaprl/refiner/reflib/term_dtable.ml
+1 -2 metaprl/refiner/reflib/term_match_table.ml
+1 -2 metaprl/refiner/reflib/term_stable.ml
+1 -2 metaprl/refiner/reflib/term_table.ml
+1 -2 metaprl/refiner/reflib/theory.ml
+1 -2 metaprl/refiner/rewrite/rewrite.ml
+1 -2 metaprl/refiner/rewrite/rewrite_build_contractum.ml
+1 -2 metaprl/refiner/rewrite/rewrite_compile_contractum.ml
+1 -2 metaprl/refiner/rewrite/rewrite_compile_redex.ml
+1 -2 metaprl/refiner/rewrite/rewrite_debug.ml
+1 -2 metaprl/refiner/rewrite/rewrite_match_redex.ml
+1 -2 metaprl/refiner/rewrite/rewrite_util.ml
+1 -2 metaprl/refiner/term_ds/term_base_ds.ml
+1 -2 metaprl/refiner/term_ds/term_ds.ml
+1 -2 metaprl/refiner/term_ds/term_man_ds.ml
+1 -2 metaprl/refiner/term_ds/term_subst_ds.ml
+1 -2 metaprl/refiner/term_gen/term_man_gen.ml
+1 -2 metaprl/refiner/term_std/term_base_std.ml
+1 -2 metaprl/refiner/term_std/term_std.ml
+1 -2 metaprl/refiner/term_std/term_subst_std.ml
+1 -2 metaprl/theories/base/base_auto_tactic.ml
+1 -2 metaprl/theories/base/base_dform.ml
+1 -2 metaprl/theories/base/base_dtactic.ml
+1 -2 metaprl/theories/base/summary.ml
+1 -2 metaprl/theories/base/typeinf.ml
+1 -2 metaprl/theories/czf/czf_itt_all.ml
+1 -2 metaprl/theories/czf/czf_itt_and.ml
+1 -2 metaprl/theories/czf/czf_itt_axioms.ml
+1 -2 metaprl/theories/czf/czf_itt_dall.ml
+1 -2 metaprl/theories/czf/czf_itt_dexists.ml
+1 -2 metaprl/theories/czf/czf_itt_empty.ml
+1 -2 metaprl/theories/czf/czf_itt_exists.ml
+1 -2 metaprl/theories/czf/czf_itt_false.ml
+1 -2 metaprl/theories/czf/czf_itt_implies.ml
+1 -2 metaprl/theories/czf/czf_itt_or.ml
+1 -2 metaprl/theories/czf/czf_itt_pre_set.ml
+1 -2 metaprl/theories/czf/czf_itt_sall.ml
+1 -2 metaprl/theories/czf/czf_itt_sep.ml
+1 -2 metaprl/theories/czf/czf_itt_set.ml
+1 -2 metaprl/theories/czf/czf_itt_set_ext.ml
+1 -2 metaprl/theories/czf/czf_itt_set_ind.ml
+1 -2 metaprl/theories/czf/czf_itt_sexists.ml
+1 -2 metaprl/theories/czf/czf_itt_small.ml
+1 -2 metaprl/theories/czf/czf_itt_true.ml
+1 -2 metaprl/theories/czf/czf_itt_union.ml
+1 -2 metaprl/theories/itt/itt_arith.ml
+1 -2 metaprl/theories/itt/itt_atom.ml
+1 -2 metaprl/theories/itt/itt_decidable.ml
+1 -2 metaprl/theories/itt/itt_dfun.ml
+1 -2 metaprl/theories/itt/itt_dprod.ml
+1 -2 metaprl/theories/itt/itt_dprod_imp.ml
+1 -2 metaprl/theories/itt/itt_equal.ml
+1 -2 metaprl/theories/itt/itt_ext_equal.ml
+1 -2 metaprl/theories/itt/itt_fun.ml
+1 -2 metaprl/theories/itt/itt_int.ml
+1 -2 metaprl/theories/itt/itt_isect.ml
+1 -2 metaprl/theories/itt/itt_list.ml
+1 -2 metaprl/theories/itt/itt_logic.ml
+1 -2 metaprl/theories/itt/itt_prec.ml
+1 -2 metaprl/theories/itt/itt_prod.ml
+1 -2 metaprl/theories/itt/itt_quotient.ml
+1 -2 metaprl/theories/itt/itt_rfun.ml
+1 -2 metaprl/theories/itt/itt_set.ml
+1 -2 metaprl/theories/itt/itt_squash.ml
+1 -2 metaprl/theories/itt/itt_srec.ml
+1 -2 metaprl/theories/itt/itt_struct.ml
+1 -2 metaprl/theories/itt/itt_subtype.ml
+1 -2 metaprl/theories/itt/itt_union.ml
+1 -2 metaprl/theories/itt/itt_unit.ml
+1 -2 metaprl/theories/itt/itt_void.ml
+1 -2 metaprl/theories/itt/main.ml
+1 -2 metaprl/theories/ocaml/ocaml_base_df.ml
+1 -2 metaprl/theories/ocaml/ocaml_expr_df.ml
+1 -2 metaprl/theories/ocaml/ocaml_me_df.ml
+1 -2 metaprl/theories/ocaml/ocaml_mt_df.ml
+1 -2 metaprl/theories/ocaml/ocaml_patt_df.ml
+1 -2 metaprl/theories/ocaml/ocaml_sig_df.ml
+1 -2 metaprl/theories/ocaml/ocaml_str_df.ml
+1 -2 metaprl/theories/ocaml/ocaml_type_df.ml
+1 -2 metaprl/theories/ocaml_sos/ocaml_expr_sos.ml
+1 -2 metaprl/theories/ocaml_sos/ocaml_logic.ml
+1 -2 metaprl/theories/ocaml_sos/ocaml_me_sos.ml
+1 -2 metaprl/theories/ocaml_sos/ocaml_mt_sos.ml
+1 -2 metaprl/theories/ocaml_sos/ocaml_patt_sos.ml
+1 -2 metaprl/theories/ocaml_sos/ocaml_sig_sos.ml
+1 -2 metaprl/theories/ocaml_sos/ocaml_str_sos.ml
+1 -2 metaprl/theories/ocaml_sos/ocaml_type_sos.ml
+1 -2 metaprl/theories/tactic/nuprl_font.ml
+1 -2 metaprl/theories/tactic/perv.ml
+1 -2 metaprl/theories/tactic/tactic_cache.ml
+1 -2 metaprl/theories/tactic/top_conversionals.ml
+1 -2 metaprl/theories/tactic/var.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-10-23 11:54:50 -0700 (Sat, 23 Oct 1999)
Revision: 2823
Log message:

      Frameset for mp-people.html
      

Changes  Path
Added metaprl/doc/htmlman/people.html
Properties metaprl/doc/htmlman/people.html

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-10-25 14:45:17 -0700 (Mon, 25 Oct 1999)
Revision: 2824
Log message:

      I created a Makefile that allows converting MetaPRL documentatoion into
      PS and PDF format using HTMLDOC utility.
      
      Curenntly three pairs of (.PS,.PDF) files are being created:
      introduction - introduction to MetaPRL, installing MetaPRl, etc
      user-guide - User Guide
      tutorial - MetaPRL Tutorial
      
      I had to modify html files slightly (mostly - H1-H6 tags) to help HTMLDOC
      better understand the structure.
      

Changes  Path
Properties metaprl/doc
Added metaprl/doc/Makefile
Properties metaprl/doc/Makefile
+2 -2 metaprl/doc/htmlman/license.html
+2 -2 metaprl/doc/htmlman/mp-frame.html
+4 -3 metaprl/doc/htmlman/mp-install.html
+1 -1 metaprl/doc/htmlman/mp-links.html
+1 -1 metaprl/doc/htmlman/mp-people.html
+4 -3 metaprl/doc/htmlman/mp.html
+1 -0 metaprl/doc/htmlman/tutorial/mp-all.html
+3 -2 metaprl/doc/htmlman/tutorial/mp-base-auto.html
+5 -4 metaprl/doc/htmlman/tutorial/mp-base.html
+1 -0 metaprl/doc/htmlman/tutorial/mp-class.html
+1 -0 metaprl/doc/htmlman/tutorial/mp-ctheory.html
+2 -1 metaprl/doc/htmlman/tutorial/mp-not.html
+1 -0 metaprl/doc/htmlman/tutorial/mp-simple.html
+1 -0 metaprl/doc/htmlman/tutorial/mp-struct.html
+1 -0 metaprl/doc/htmlman/tutorial/mp-theory.html
+4 -3 metaprl/doc/htmlman/user-guide/mp-axiom.html
+7 -6 metaprl/doc/htmlman/user-guide/mp-dform.html
+6 -5 metaprl/doc/htmlman/user-guide/mp-editor.html
+2 -1 metaprl/doc/htmlman/user-guide/mp-modules.html
+4 -3 metaprl/doc/htmlman/user-guide/mp-rewrite.html
+9 -8 metaprl/doc/htmlman/user-guide/mp-terms.html

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-10-25 19:44:44 -0700 (Mon, 25 Oct 1999)
Revision: 2825
Log message:

      - Added a Makefile target "check" that checks HTML syntax
      using weblint utility ( http://www.weblint.org/ )
      
      - Fixed most of the HTML problems reported by weblint utility
      This reduced the number of weblint warnings from over 8000 to 19
      (All 19 are
         unknown attribute "..." for element <FRAMESET>
      where ... is either FRAMEBORDER, BORDER or FRAMESPACING)
      
      - Added system.{ps,pdf} (MetaPRL System Description)
      to the list of generated documentation files
      
      - Some htmldoc-related fixes
      
      - Removed the references to "load" command since
      in the current version of MetaPRL "cd" command loads
      the module if necessary.
      
      - Removed some unused test files
      

Changes  Path
+1 -1 metaprl/Makefile
+33 -1 metaprl/doc/Makefile
+117 -112 metaprl/doc/htmlman/chars/table.html
+1 -1 metaprl/doc/htmlman/framework/mp-framework.html
+3 -3 metaprl/doc/htmlman/framework/mp-index.html
Added metaprl/doc/htmlman/goals.html
Properties metaprl/doc/htmlman/goals.html
+4 -4 metaprl/doc/htmlman/license.html
+2 -2 metaprl/doc/htmlman/mp-cvs-rw.html
+1 -1 metaprl/doc/htmlman/mp-frame.html
+3 -4 metaprl/doc/htmlman/mp-index.html
+1 -1 metaprl/doc/htmlman/mp-install.html
+1 -1 metaprl/doc/htmlman/mp-links.html
+1 -1 metaprl/doc/htmlman/mp-people.html
+4 -4 metaprl/doc/htmlman/mp.html
Deleted metaprl/doc/htmlman/system/mp-arch.html
+1 -1 metaprl/doc/htmlman/system/mp-auto-tactic.html
+1 -1 metaprl/doc/htmlman/system/mp-base-cache.html
+178 -178 metaprl/doc/htmlman/system/mp-base-syntax.html
+1 -1 metaprl/doc/htmlman/system/mp-base.html
+1 -1 metaprl/doc/htmlman/system/mp-chaining.html
+5 -5 metaprl/doc/htmlman/system/mp-conversionals.html
Deleted metaprl/doc/htmlman/system/mp-dist-tactic.html
+4 -4 metaprl/doc/htmlman/system/mp-editor-imp.html
+31 -31 metaprl/doc/htmlman/system/mp-ensemble.html
+1 -1 metaprl/doc/htmlman/system/mp-filter.html
+4 -5 metaprl/doc/htmlman/system/mp-index.html
+3 -3 metaprl/doc/htmlman/system/mp-itt.html
+1 -1 metaprl/doc/htmlman/system/mp-ocaml.html
+5 -5 metaprl/doc/htmlman/system/mp-refine.html
+1 -1 metaprl/doc/htmlman/system/mp-refiner.html
+1 -1 metaprl/doc/htmlman/system/mp-rewrite.html
+14 -13 metaprl/doc/htmlman/system/mp-system.html
+2 -2 metaprl/doc/htmlman/system/mp-tactic.html
+7 -8 metaprl/doc/htmlman/system/mp-tacticals.html
+1 -1 metaprl/doc/htmlman/system/mp-terms.html
+1 -1 metaprl/doc/htmlman/system/mp-type-inf-rsrc.html
Deleted metaprl/doc/htmlman/system/table.html
+1 -3 metaprl/doc/htmlman/tutorial/mp-all.html
+1 -1 metaprl/doc/htmlman/tutorial/mp-base-auto.html
+1 -1 metaprl/doc/htmlman/tutorial/mp-base.html
+1 -1 metaprl/doc/htmlman/tutorial/mp-class.html
+9 -9 metaprl/doc/htmlman/tutorial/mp-ctheory.html
+1 -1 metaprl/doc/htmlman/tutorial/mp-getting-started.html
+4 -5 metaprl/doc/htmlman/tutorial/mp-index.html
+25 -25 metaprl/doc/htmlman/tutorial/mp-not.html
+3 -3 metaprl/doc/htmlman/tutorial/mp-simple.html
+1 -1 metaprl/doc/htmlman/tutorial/mp-struct.html
+13 -13 metaprl/doc/htmlman/tutorial/mp-theory.html
+1 -1 metaprl/doc/htmlman/tutorial/mp-tutorial.html
+3 -3 metaprl/doc/htmlman/tutorial/mp-type.html
+4 -4 metaprl/doc/htmlman/user-guide/mp-axiom.html
+702 -919 metaprl/doc/htmlman/user-guide/mp-dform.html
+1464 -1924 metaprl/doc/htmlman/user-guide/mp-editor.html
+3 -3 metaprl/doc/htmlman/user-guide/mp-index.html
+1 -1 metaprl/doc/htmlman/user-guide/mp-modules.html
+4 -4 metaprl/doc/htmlman/user-guide/mp-rewrite.html
+1 -1 metaprl/doc/htmlman/user-guide/mp-terms.html
+1 -1 metaprl/doc/htmlman/user-guide/mp-user-guide.html
Deleted metaprl/doc/htmlman/user-guide/x.html
+19 -19 metaprl/doc/term_ds_types.html
Added metaprl/doc/weblintrc
Properties metaprl/doc/weblintrc

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-10-26 13:47:53 -0700 (Tue, 26 Oct 1999)
Revision: 2826
Log message:

      - Added documentation on how to convert documentation .PS and .PDF formats.
      
      - Removed mp-frame.html - as far as I can see, it is just an outdated
      version of mp.html
      
      - Added more HTML files to system.{ps,pdf}
      

Changes  Path
+5 -0 metaprl/Makefile
+8 -3 metaprl/doc/Makefile
Deleted metaprl/doc/htmlman/mp-frame.html
+4 -1 metaprl/doc/htmlman/mp-install.html
+5 -2 metaprl/doc/htmlman/mp-people.html
+5 -1 metaprl/doc/htmlman/mp.html
+2 -1 metaprl/doc/htmlman/system/mp-auto-tactic.html
+1 -1 metaprl/doc/htmlman/system/mp-base-cache.html
+113 -113 metaprl/doc/htmlman/system/mp-base-syntax.html
+1 -1 metaprl/doc/htmlman/system/mp-type-inf-rsrc.html

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-10-26 15:14:51 -0700 (Tue, 26 Oct 1999)
Revision: 2828
Log message:

      Renamed break -> hbreak (dforms construction) to be more consistent.
      

Changes  Path
+5 -5 metaprl/doc/htmlman/user-guide/mp-dform.html
+1 -1 metaprl/filter/base/filter_cache_fun.ml
+6 -6 metaprl/refiner/reflib/dform.ml
+3 -3 metaprl/refiner/reflib/rformat.ml
+2 -2 metaprl/refiner/reflib/rformat.mli
+11 -11 metaprl/theories/base/base_dform.ml
+1 -1 metaprl/theories/base/summary.ml
+1 -1 metaprl/theories/itt/itt_sort.ml
+4 -4 metaprl/theories/ocaml/ocaml_expr_df.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-10-26 15:19:30 -0700 (Tue, 26 Oct 1999)
Revision: 2829
Log message:

      Small fixes.
      

Changes  Path
+1 -1 metaprl/doc/htmlman/system/mp-terms.html
+5 -8 metaprl/doc/htmlman/user-guide/mp-dform.html
+19 -20 metaprl/doc/htmlman/user-guide/mp-terms.html

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-10-26 22:41:35 -0700 (Tue, 26 Oct 1999)
Revision: 2830
Log message:

      More fixes
      
      I have finished proof-reading the introduction and the user's guide and
      I still have tutorial and system description left.
      

Changes  Path
+2 -1 metaprl/BUGS
+1 -1 metaprl/doc/Makefile
+36 -38 metaprl/doc/htmlman/user-guide/mp-axiom.html
+15 -17 metaprl/doc/htmlman/user-guide/mp-editor.html
+8 -9 metaprl/doc/htmlman/user-guide/mp-modules.html
+7 -14 metaprl/doc/htmlman/user-guide/mp-rewrite.html
+3 -3 metaprl/doc/htmlman/user-guide/mp-user-guide.html

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-10-27 09:42:06 -0700 (Wed, 27 Oct 1999)
Revision: 2831
Log message:

      HTMLDOC does not like "<PRE><IMG ...></PRE>.
      Since in this context <PRE> is unnecessary, I removed it.
      

Changes  Path
+8 -8 metaprl/doc/htmlman/tutorial/mp-ctheory.html
+22 -22 metaprl/doc/htmlman/tutorial/mp-not.html
+2 -2 metaprl/doc/htmlman/tutorial/mp-simple.html
+2 -2 metaprl/doc/htmlman/tutorial/mp-type.html

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-10-27 09:56:52 -0700 (Wed, 27 Oct 1999)
Revision: 2832
Log message:

      Mentioned http://www.cs.cornell.edu/nogin/RPM/meta-prl/ByName.html
      

Changes  Path
+3 -1 metaprl/doc/htmlman/mp-install.html

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-10-27 16:11:27 -0700 (Wed, 27 Oct 1999)
Revision: 2833
Log message:

      Added a warning:
      
      <P><I><B>Warning:</B> This tutorial is a little outdated.</I> Most things would probably
      still work as described, but we have implemented several mechanisms (such as resource
      annotations) that are much easier to use than the mechanisms used in this tutorial.</P>
      

Changes  Path
+3 -0 metaprl/doc/htmlman/tutorial/mp-tutorial.html

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-10-27 16:27:52 -0700 (Wed, 27 Oct 1999)
Revision: 2834
Log message:

      Added:
      
      This file was contributed by Carl R. Witty <cwitty@newtonlabs.com>
      

Changes  Path
+1 -0 metaprl/doc/itt_quickref.txt

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-10-31 16:10:29 -0800 (Sun, 31 Oct 1999)
Revision: 2835
Log message:

      Some formatting fixes
      

Changes  Path
+6 -6 metaprl/doc/htmlman/license.html
+1 -1 metaprl/doc/htmlman/mp-people.html
+1 -1 metaprl/doc/htmlman/mp.html
+12 -12 metaprl/doc/htmlman/system/mp-ensemble.html
+2 -2 metaprl/doc/htmlman/system/mp-itt.html
+1 -1 metaprl/doc/htmlman/system/mp-system.html
+2 -0 metaprl/doc/weblintrc

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-10-31 18:04:09 -0800 (Sun, 31 Oct 1999)
Revision: 2836
Log message:

      Fixed some links, updated some information, added rwhigher info.
      

Changes  Path
+3 -3 metaprl/doc/htmlman/system/mp-index.html
+19 -15 metaprl/doc/htmlman/system/mp-refine.html
+7 -3 metaprl/doc/htmlman/system/mp-refiner.html
+2 -2 metaprl/doc/htmlman/system/mp-rewrite.html
+5 -4 metaprl/doc/htmlman/system/mp-terms.html
+4 -4 metaprl/doc/htmlman/tutorial/mp-index.html
+4 -4 metaprl/doc/htmlman/user-guide/mp-index.html