[nogin] When opnames do not match, raise RefineError directly_ Mon Sep 19 02:01:13 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-13-415863000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-13-415863000-PDT.html [nogin] Replaced 80 with 100_ Mon Sep 19 02:01:14 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-14-766819000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-14-766819000-PDT.html [jyh] Refiner modules now raise RefineError exceptions directly._ Mon Sep 19 02:01:15 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-15-448710000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-15-448710000-PDT.html [jyh] Created term_copy module to copy and normalize terms._ Mon Sep 19 02:01:32 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-32-554471000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-32-554471000-PDT.html [nogin] Allow changing the ocamlopt _inline option with the INLINE environment variable_ Mon Sep 19 02:01:36 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-36-894908000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-36-894908000-PDT.html [nogin] Added __ROOT_/refiner/refsig/refine_error.h to the list_ Mon Sep 19 02:01:37 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-37-242043000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-37-242043000-PDT.html [nogin] Divided refine.ml into a _verbose_ and a _simple_ versions._ Mon Sep 19 02:01:37 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-37-591405000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-37-591405000-PDT.html [nogin] ._ Mon Sep 19 02:01:39 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-39-865431000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-39-865431000-PDT.html [nogin] Fixed a small bug _ thanks to Steve Zdancewic._ Mon Sep 19 02:01:40 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-40-324240000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-40-324240000-PDT.html [nogin] Specified the full _path_ to the Refine module__ Mon Sep 19 02:01:41 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-41-745847000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-41-745847000-PDT.html [jyh] IO terms are now in term_std format._ Mon Sep 19 02:01:42 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-42-355079000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-42-355079000-PDT.html [nogin] Removed some unused files_ Mon Sep 19 02:01:45 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-45-416147000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-45-416147000-PDT.html [nogin] Added _S option_ Mon Sep 19 02:01:45 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-45-831523000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-45-831523000-PDT.html [nogin] Do not be too verbose in case orelseT fails_ Mon Sep 19 02:01:46 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-46-211980000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-46-211980000-PDT.html [nogin] Made make_term function 40_ faster._ Mon Sep 19 02:01:46 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-46-595850000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-46-595850000-PDT.html [nogin] Fixed mk_so_var _ it should not use mk_term_ Mon Sep 19 02:01:46 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-46-957037000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-46-957037000-PDT.html [nogin] Set GC parameters_ Mon Sep 19 02:01:47 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-47-372792000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-47-372792000-PDT.html [nogin] Use fact_125__ Mon Sep 19 02:01:47 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-47-830014000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-47-830014000-PDT.html [nogin] mk_term should be able to handle the case wher opname __ var_opname _ ocaml_df uses it._ Mon Sep 19 02:01:48 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-48-196036000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-48-196036000-PDT.html [jyh] Itt_theory.ml_,i_ are now different._ Mon Sep 19 02:01:48 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-48-553827000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-48-553827000-PDT.html [nogin] Rewrote var_subst to make it do what it is actually supposed to do_ Mon Sep 19 02:01:48 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-48-996726000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-48-996726000-PDT.html [nogin] Finally _make _j_ and _make _j opt_ do everything right_ Mon Sep 19 02:01:49 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-49-392586000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-49-392586000-PDT.html [nogin] Better Makefiles_ Mon Sep 19 02:01:49 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-49-755051000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-49-755051000-PDT.html [nogin] Do not pass unnecessary arguments in a _simple version of the refiner_ Mon Sep 19 02:01:50 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-50-162670000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-50-162670000-PDT.html [nogin] Compile with _noassert by default._ Mon Sep 19 02:01:51 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-51-031231000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-51-031231000-PDT.html [nogin] Added _noassert option to prlc_ Mon Sep 19 02:01:51 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-51-609304000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-51-609304000-PDT.html [nogin] Removed _Log messages from all NL files._ Mon Sep 19 02:01:51 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-51-994525000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-01-51-994525000-PDT.html [nogin] Created an alternative apply_fun[_arg]_at_addr for functions that do not depend on bvars list._ Mon Sep 19 02:02:09 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-09-579531000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-09-579531000-PDT.html [jyh] Working czf_itt_set._ Mon Sep 19 02:02:10 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-10-180542000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-10-180542000-PDT.html [nogin] Test the new CVS server_ Mon Sep 19 02:02:13 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-13-565108000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-13-565108000-PDT.html [jyh] Test._ Mon Sep 19 02:02:13 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-13-913646000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-13-913646000-PDT.html [nogin] Moved all _if _debug_..._ statements in the refiner_ Mon Sep 19 02:02:14 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-14-254498000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-14-254498000-PDT.html [nogin] Added apply_fun_higher _ _term __ term _ _a_ __ term __ term _ _a list_ Mon Sep 19 02:02:15 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-15-091568000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-15-091568000-PDT.html [jyh] Pushed higherC into the refiner for efficiency._ Mon Sep 19 02:02:15 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-15-555357000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-15-555357000-PDT.html [jyh] Fixed firstC to enable higherC optimization._ Mon Sep 19 02:02:19 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-19-578431000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-19-578431000-PDT.html [jyh] Fixed a missing case in firstC._ Mon Sep 19 02:02:20 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-20-009519000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-20-009519000-PDT.html [nogin] Use fact_250_ instead of fact_125_._ Mon Sep 19 02:02:20 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-20-373275000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-20-373275000-PDT.html [nogin] Do not allocate a cons cell before calling apply_rewrite or apply_redex __ Mon Sep 19 02:02:20 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-20-744171000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-20-744171000-PDT.html [nogin] Create _[__], [__], []_ and _[__], [__]_ in advance, not at every call_ Mon Sep 19 02:02:21 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-21-556315000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-21-556315000-PDT.html [jyh] Upgraded czf._ Mon Sep 19 02:02:21 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-21-961038000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-21-961038000-PDT.html [nogin] Faster opname_of_term_ Mon Sep 19 02:02:23 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-23-897422000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-23-897422000-PDT.html [nogin] Faster alpha_equal_ Mon Sep 19 02:02:24 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-24-274842000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-24-274842000-PDT.html [eli] Corrected CAMLLIB location in README._ Mon Sep 19 02:02:24 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-24-660888000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-24-660888000-PDT.html [nogin] CAMLLIB _ CAMLP4LIB directories should be set to_ Mon Sep 19 02:02:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-25-733830000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-25-733830000-PDT.html [jyh] Intermediate version with auto tactic._ Mon Sep 19 02:02:26 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-26-318578000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-26-318578000-PDT.html [jyh] Added to itt_derived._ Mon Sep 19 02:02:33 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-33-372069000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-33-372069000-PDT.html [nogin] Use fact_300__ Mon Sep 19 02:02:34 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-34-107613000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-34-107613000-PDT.html [nogin] Better alpha_equal_ Mon Sep 19 02:02:34 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-34-726923000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-34-726923000-PDT.html [jyh] Extensions to unix library._ Mon Sep 19 02:02:35 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-35-207269000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-35-207269000-PDT.html [nogin] apply_fun_higher was making some unnecessary calls to mk_bterm _ fixed._ Mon Sep 19 02:02:35 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-35-611823000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-35-611823000-PDT.html [nogin] Faster alpha_equal_ Mon Sep 19 02:02:36 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-36-075116000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-36-075116000-PDT.html [nogin] Faster match_redex_ Mon Sep 19 02:02:36 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-36-468152000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-36-468152000-PDT.html [jyh] CZF is complete, although we may wish to add pairing and inf._ Mon Sep 19 02:02:37 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-37-044630000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-37-044630000-PDT.html [nogin] I am testing the new e_mail notification scripts._ Mon Sep 19 02:02:41 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-41-062588000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-41-062588000-PDT.html [nogin] Use Failure instead of Invalid_argument_ Mon Sep 19 02:02:41 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-41-492558000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-41-492558000-PDT.html [jyh] Added NL toploop so that we can compile NL native code._ Mon Sep 19 02:02:42 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-42-890428000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-42-890428000-PDT.html [jyh] Removed dest_sequent, and changed Term_man_sig.esequent to use arrays._ Mon Sep 19 02:02:52 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-52-329409000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-52-329409000-PDT.html [jyh] Changed opname equality. Opnames should be compared with_ Mon Sep 19 02:02:53 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-53-263654000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-53-263654000-PDT.html [nogin] Added _.top_ Mon Sep 19 02:02:55 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-55-256735000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-55-256735000-PDT.html [nogin] Fixed test.opt compilation_ Mon Sep 19 02:02:55 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-55-609008000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-55-609008000-PDT.html [jyh] Added the Opname.atom type. Opname.opname can be converted to_ Mon Sep 19 02:02:55 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-55-982457000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-55-982457000-PDT.html [nogin] Do not copy anything to the lib directory, use ln instead_ Mon Sep 19 02:02:56 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-56-403242000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-56-403242000-PDT.html [nogin] Do not copy anything in bin, use ln instead_ Mon Sep 19 02:02:56 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-56-825217000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-56-825217000-PDT.html [nogin] Make _make clean_ really clean _ remove _.run _.cma and _.cmxa files_ Mon Sep 19 02:02:57 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-57-199312000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-57-199312000-PDT.html [nogin] Oops, forgot _.cmx_ Mon Sep 19 02:02:57 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-57-601189000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-57-601189000-PDT.html [nogin] Removed CVS _Log messages_ Mon Sep 19 02:02:57 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-57-973731000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-57-973731000-PDT.html [nogin] Moved eseqent type to the TermType module._ Mon Sep 19 02:02:58 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-58-708388000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-58-708388000-PDT.html [nogin] Term_copy now checks if the term is a sequent _with is_sequent_term__ Mon Sep 19 02:02:59 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-59-605031000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-02-59-605031000-PDT.html [jyh] Exceptions reported properly in filter_main._ Mon Sep 19 02:03:00 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-00-183201000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-00-183201000-PDT.html [jyh] Fixed exception reporting in Filter_parse.MakeFilter.save._ Mon Sep 19 02:03:00 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-00-554281000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-00-554281000-PDT.html [jyh] Removed rewriteContextCut. This needs to be reimplemented._ Mon Sep 19 02:03:01 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-01-811438000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-01-811438000-PDT.html [nogin] Commented out some sequent code that should be rewritten._ Mon Sep 19 02:03:02 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-02-225940000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-02-225940000-PDT.html [nogin] Fixed some typos_ Mon Sep 19 02:03:02 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-02-988868000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-02-988868000-PDT.html [nogin] Fixed some other typos_ Mon Sep 19 02:03:03 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-03-366856000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-03-366856000-PDT.html [nogin] Renamed Refine_ds to Refine_ds_verb and Refine_std to Refine_std_verb_ Mon Sep 19 02:03:03 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-03-771057000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-03-771057000-PDT.html [nogin] Functorized the Simple_print module over the Refiner module_ Mon Sep 19 02:03:04 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-04-525039000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-04-525039000-PDT.html [nogin] Functorized term_copy module over the whole refiner instead of over seperate term modules_ Mon Sep 19 02:03:05 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-05-955256000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-05-955256000-PDT.html [jyh] Added debugging to copy_proof._ Mon Sep 19 02:03:06 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-06-727927000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-06-727927000-PDT.html [nogin] ._ Mon Sep 19 02:03:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-07-134155000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-07-134155000-PDT.html [nogin] Fixed a bug_ Mon Sep 19 02:03:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-07-525578000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-07-525578000-PDT.html [jyh] Updated .prlb files._ Mon Sep 19 02:03:08 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-08-113845000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-08-113845000-PDT.html [nogin] Fixed nl.run full toploop compilation_ Mon Sep 19 02:03:08 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-08-622571000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-08-622571000-PDT.html [nogin] No need to make opt twice in editor/ml_ Mon Sep 19 02:03:09 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-09-016120000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-09-016120000-PDT.html [nogin] Changed the default camlp4 directory to /usr/lib/camlp4_ Mon Sep 19 02:03:09 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-09-383936000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-09-383936000-PDT.html [nogin] If CAMLLIB is not defined, use /usr/lib/ocaml_ Mon Sep 19 02:03:09 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-09-769172000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-09-769172000-PDT.html [nogin] Added a new function get_core that is supposed to know how to push down_ Mon Sep 19 02:03:10 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-10-141481000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-10-141481000-PDT.html [nogin] Use __RM_ instead of del or rm _f_ Mon Sep 19 02:03:10 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-10-918947000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-10-918947000-PDT.html [nogin] Faster filter functions _ preserve sharing when possible_ Mon Sep 19 02:03:11 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-11-551187000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-11-551187000-PDT.html [nogin] Initial checkin _ TermMan module for_ Mon Sep 19 02:03:11 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-11-949907000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-11-949907000-PDT.html [nogin] Better cpp macros _ML code should not have been changed__ Mon Sep 19 02:03:12 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-12-610927000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-12-610927000-PDT.html [nogin] Changed the Term_ds module to treat sequents specially._ Mon Sep 19 02:03:13 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-13-025243000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-13-025243000-PDT.html [nogin] Sequent_aware alpha_equality_ Mon Sep 19 02:03:14 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-14-193293000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-14-193293000-PDT.html [nogin] Added optimized code profiled compilation _make profile__ Mon Sep 19 02:03:14 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-14-637735000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-14-637735000-PDT.html [nogin] Faster opname_of_term_ Mon Sep 19 02:03:15 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-15-018954000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-15-018954000-PDT.html [jyh] Updated occurs_check in unification._ Mon Sep 19 02:03:15 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-15-434832000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-15-434832000-PDT.html [jyh] Added TPTP theory, and Ensemble library. Fixed sequent displays._ Mon Sep 19 02:03:16 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-16-082589000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-16-082589000-PDT.html [jyh] Updated indentation style in term_man_ds.mlp_ Mon Sep 19 02:03:21 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-21-070109000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-21-070109000-PDT.html [nogin] In Term_ds module is__ functions should use get_core instead of dest_term_ Mon Sep 19 02:03:21 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-21-679659000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-21-679659000-PDT.html [nogin] Added functions append_array and append_list to SeqHyp and SeqGoal modules_ Mon Sep 19 02:03:22 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-22-584310000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/1998-07/2005-09-19-02-03-22-584310000-PDT.html