[jyh] Update to match libmojave._ Mon Sep 19 07:20:57 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-20-57-362441000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-20-57-362441000-PDT.html [nogin] _ Use omake_s internal digest function for magic number computation in_ Mon Sep 19 07:20:57 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-20-57-737257000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-20-57-737257000-PDT.html [nogin] Give an error message reading _not enough information to infer the type of the_ Mon Sep 19 07:20:58 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-20-58-250688000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-20-58-250688000-PDT.html [nogin] When a free variable is encountered where a hypothesis type is expected, just_ Mon Sep 19 07:20:58 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-20-58-708859000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-20-58-708859000-PDT.html [nogin] Attempt and making the ASCII syntax documentation a bit more clear._ Mon Sep 19 07:20:59 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-20-59-165470000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-20-59-165470000-PDT.html [yegor] removed references to Cic_ind_elim_prodH _which does nto exist__ Mon Sep 19 07:20:59 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-20-59-551761000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-20-59-551761000-PDT.html [nogin] Ignore .omakedb.lock_ Mon Sep 19 07:20:59 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-20-59-941454000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-20-59-941454000-PDT.html [nogin] Updated to support more browsers._ Mon Sep 19 07:21:00 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-00-280880000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-00-280880000-PDT.html [nogin] Adding a missing line to the HOSC paper._ Mon Sep 19 07:21:00 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-00-631724000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-00-631724000-PDT.html [nogin] Renamed Ocaml_OCaml __ Ocaml_TyOCaml _to avoid clashes with Comment_OCaml_._ Mon Sep 19 07:21:01 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-01-044211000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-01-044211000-PDT.html [nogin] Fixed a display form that broke recently._ Mon Sep 19 07:21:02 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-02-515426000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-02-515426000-PDT.html [yegor] removed _stray_ prodH declaration_ Mon Sep 19 07:21:02 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-02-880581000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-02-880581000-PDT.html [yegor] Some fixes in display forms_ Mon Sep 19 07:21:03 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-03-225696000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-03-225696000-PDT.html [nogin] Removing itt_eq_base _ this idea did not work out._ Mon Sep 19 07:21:03 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-03-624486000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-03-624486000-PDT.html [yegor] Typing of induction elimination operation _primitive recursion_ is complete_ Mon Sep 19 07:21:05 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-05-197642000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-05-197642000-PDT.html [] This commit was manufactured by cvs2svn to create branch _new_scanner2_._ Mon Sep 19 07:21:05 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-05-834002000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-05-834002000-PDT.html [yegor] First approximation of conversion rule for _primitive_ recursion operation._ Mon Sep 19 07:21:21 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-21-666413000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-21-666413000-PDT.html [jyh] Changes to match the scanner changes in omake._ Mon Sep 19 07:21:22 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-22-770498000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-22-770498000-PDT.html [jyh] Removed the PRLFiles function. For now, directories that have a mix_ Mon Sep 19 07:21:23 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-23-939047000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-23-939047000-PDT.html [jyh] New method for computing theories.dir and mldebug.dir _the search_ Mon Sep 19 07:21:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-25-108796000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-25-108796000-PDT.html [nogin] Removing some leftover Phobos stuff._ Mon Sep 19 07:21:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-25-775381000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-25-775381000-PDT.html [nogin] A _uniformity_ pass over the OMakefiles__ Mon Sep 19 07:21:26 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-26-227931000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-26-227931000-PDT.html [nogin] Added ___ input shortcut for _iff_._ Mon Sep 19 07:21:28 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-28-944183000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-28-944183000-PDT.html [nogin] ToploopIgnoreError/ToploopIgnoreExn should not cause the http server to die._ Mon Sep 19 07:21:29 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-29-501924000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-29-501924000-PDT.html [nogin] The exception wrappers in filter_exn and refine_exn were turning all_ Mon Sep 19 07:21:29 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-29-996247000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-29-996247000-PDT.html [nogin] Adding the image type._ Mon Sep 19 07:21:30 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-30-459302000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-30-459302000-PDT.html [nogin] Derived the union type from the image type._ Mon Sep 19 07:21:33 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-33-266013000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-33-266013000-PDT.html [nogin] Fixed a build issue caused by an empty [OPT]THREADSLIB variable in an array,_ Mon Sep 19 07:21:37 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-37-480638000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-37-480638000-PDT.html [jyh] This is an update to match the recent changes to omake. This is_ Mon Sep 19 07:21:37 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-37-890562000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-37-890562000-PDT.html [nogin] Moved list_max from Itt_nat into Itt_list2._ Mon Sep 19 07:21:38 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-38-867195000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-38-867195000-PDT.html [nogin] _ Fixed a few minor OMakefile issues left over from the new_scanner branch_ Mon Sep 19 07:21:48 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-48-770490000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-48-770490000-PDT.html [jyh] For some reason, we never exported the Win32 anti_configuration_ Mon Sep 19 07:21:49 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-49-293771000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-49-293771000-PDT.html [jyh] Removed some Win32_specific variables that are no longer needed._ Mon Sep 19 07:21:49 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-49-667188000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-49-667188000-PDT.html [nogin] No need to shadow scan_ocaml__ rules with almost identical one _we used to_ Mon Sep 19 07:21:50 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-50-110148000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-50-110148000-PDT.html [nogin] Itt_nat.nat_is_int needed an nth_hyp annotation._ Mon Sep 19 07:21:50 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-50-479494000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-50-479494000-PDT.html [nogin] Ignore .omakedb.lock on realclean._ Mon Sep 19 07:21:50 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-50-849308000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-50-849308000-PDT.html [nogin] Added a theory of abstract operators for HOAS._ Mon Sep 19 07:21:51 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-51-209659000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-51-209659000-PDT.html [nogin] Added a theory of the basic purely computational HOAS_ Mon Sep 19 07:21:53 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-53-226749000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-53-226749000-PDT.html [nogin] I added a HACK to make it unnecessary to type ____ all the time on the CLI__ Mon Sep 19 07:21:54 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-54-766856000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-54-766856000-PDT.html [nogin] Updated the previous _NL __ ___ hack so that it does not attemt to add the_ Mon Sep 19 07:21:55 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-55-184421000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-55-184421000-PDT.html [nogin] Committed a wrong thing, please ignore the previous commit._ Mon Sep 19 07:21:55 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-55-687212000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-55-687212000-PDT.html [nogin] _ Added Itt_list2.insert_at for inserting an element into a list at the_ Mon Sep 19 07:21:56 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-56-122939000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-21-56-122939000-PDT.html [nogin] Added a theory of _vector bindings_. I still have to prove couple of theorems_ Mon Sep 19 07:22:05 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-05-187195000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-05-187195000-PDT.html [nogin] Forgot the .prla_ Mon Sep 19 07:22:05 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-05-785416000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-05-785416000-PDT.html [nogin] TeX fixes._ Mon Sep 19 07:22:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-07-910938000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-07-910938000-PDT.html [nogin] Ignore _.fls_ Mon Sep 19 07:22:08 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-08-340647000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-08-340647000-PDT.html [nogin] Clean _fls_ Mon Sep 19 07:22:08 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-08-769331000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-08-769331000-PDT.html [nogin] More minor TeX_related fixes._ Mon Sep 19 07:22:09 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-09-136968000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-09-136968000-PDT.html [kopylov] Proved a theorem in itt_hoas_vector._ Mon Sep 19 07:22:09 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-09-619426000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-09-619426000-PDT.html [nogin] Proved all the Itt_fun2 theorems _removing the lambda_sqeq stuff_._ Mon Sep 19 07:22:10 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-10-945874000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-10-945874000-PDT.html [nogin] Slightly changing the way conditional rewrites are handled _this supposed to_ Mon Sep 19 07:22:11 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-11-983250000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-11-983250000-PDT.html [nogin] Removed a bit of unused code_ Mon Sep 19 07:22:12 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-12-432521000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-12-432521000-PDT.html [nogin] The apply_var_fun_[arg_]at_addr functions were not always handling sequent_ Mon Sep 19 07:22:12 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-12-807981000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-12-807981000-PDT.html [nogin] Updated couple of proofs a bit._ Mon Sep 19 07:22:13 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-13-361339000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-13-361339000-PDT.html [nogin] Minor fixes_ Mon Sep 19 07:22:15 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-15-806371000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-15-806371000-PDT.html [nogin] Print _empty_ variables as ___._ Mon Sep 19 07:22:16 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-16-374025000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-16-374025000-PDT.html [nogin] Minor clean_up._ Mon Sep 19 07:22:17 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-17-459201000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-17-459201000-PDT.html [nogin] Free var restriction on SO variables should be more conservative _should only_ Mon Sep 19 07:22:18 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-18-238273000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-18-238273000-PDT.html [nogin] Fixed a conversion mismatch._ Mon Sep 19 07:22:18 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-18-860301000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-18-860301000-PDT.html [nogin] Non_sequent contexts _issue 384_ _ fully implemented the _simple_ case_ Mon Sep 19 07:22:19 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-19-275838000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-19-275838000-PDT.html [nogin] Fixed couple of places in JProver where terms were being compared with_ Mon Sep 19 07:22:19 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-19-852216000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-19-852216000-PDT.html [nogin] Fixing another encoding/decoding mismatch._ Mon Sep 19 07:22:20 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-20-455190000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-20-455190000-PDT.html [nogin] Debug printout of summary items _ some items were printed with a newline at_ Mon Sep 19 07:22:20 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-20-860416000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-20-860416000-PDT.html [nogin] Use Lm_symbol.eq instead of ___ more consistently._ Mon Sep 19 07:22:21 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-21-282357000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-21-282357000-PDT.html [nogin] Use proper Lm_num functions for comparing the nums _instead of_ Mon Sep 19 07:22:22 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-22-469684000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-22-469684000-PDT.html [nogin] Fixed a number of places where comparisons functions from Pervasives were used_ Mon Sep 19 07:22:22 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-22-924925000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-22-924925000-PDT.html [nogin] More fixed related to improper usage of Pervasives.compare, _, etc._ Mon Sep 19 07:22:23 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-23-756702000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-23-756702000-PDT.html [nogin] A few fixes relating to handling and display of non_sequent contexts._ Mon Sep 19 07:22:24 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-24-857983000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-24-857983000-PDT.html [nogin] Removing an unused module_ Mon Sep 19 07:22:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-25-497786000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-25-497786000-PDT.html [nogin] Finished the Vector HOAS proofs._ Mon Sep 19 07:22:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-25-926094000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-25-926094000-PDT.html [nogin] Documentation fixes__ Mon Sep 19 07:22:35 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-35-517852000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-35-517852000-PDT.html [nogin] Fixing Yegor_s Win32 issue _the usage of ___file...__ caused a _/_ vs ____ Mon Sep 19 07:22:38 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-38-018856000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-38-018856000-PDT.html [nogin] Basic deBruijn representation._ Mon Sep 19 07:22:38 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-38-400612000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-38-400612000-PDT.html [yegor] I had this on win32__ Mon Sep 19 07:22:40 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-40-024315000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-40-024315000-PDT.html [nogin] Follow_up to Yegor_s change_ just use the DIRSEP variable._ Mon Sep 19 07:22:40 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-40-443162000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-40-443162000-PDT.html [nogin] Added the enforcement of non_recursivity of definitions _i.e. of the fact that_ Mon Sep 19 07:22:40 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-40-828113000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-40-828113000-PDT.html [nogin] Defined list_of_fun _based on partial commented out definition that already_ Mon Sep 19 07:22:41 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-41-494665000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-22-41-494665000-PDT.html [nogin] Working on defining bterm destructors. It_s not immediatelly obvious how to_ Mon Sep 19 07:23:01 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-23-01-078012000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-23-01-078012000-PDT.html [nogin] Fixing a bug that caused problems building book2.dvi_ Mon Sep 19 07:23:02 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-23-02-090972000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-23-02-090972000-PDT.html [jyh] Removed the DIRSEP. But I can_t figure out where this variable_ Mon Sep 19 07:23:02 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-23-02-484917000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-23-02-484917000-PDT.html [nogin] Added a notion of vector_substitution _substitution of a list of terms for the_ Mon Sep 19 07:23:02 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-23-02-903149000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-23-02-903149000-PDT.html [jyh] The problem with exporting back to the parent is fixed by_ Mon Sep 19 07:23:04 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-23-04-918974000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-23-04-918974000-PDT.html [nogin] _ Bumping the OMakeVersion number _I_ve waited at least 20 minutes trying to_ Mon Sep 19 07:23:05 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-23-05-321897000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-23-05-321897000-PDT.html [nogin] Finished proving properties of the _subterms_ operator._ Mon Sep 19 07:23:05 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-23-05-814553000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-23-05-814553000-PDT.html [nogin] Itt_omage was using Hashtbl.hash for computing hash values of _terms_. This,_ Mon Sep 19 07:23:08 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-23-08-732989000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-23-08-732989000-PDT.html [nogin] Numerous documentation fixes__ Mon Sep 19 07:23:09 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-23-09-201609000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-23-09-201609000-PDT.html [nogin] Updated the _sequentialization of rewrtites_ hack so that when it creates_ Mon Sep 19 07:23:10 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-23-10-491552000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-23-10-491552000-PDT.html [nogin] In my previous commit, I accidentally included some temporary transition code,_ Mon Sep 19 07:26:49 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-26-49-867453000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-26-49-867453000-PDT.html [nogin] Defined the dest_term operator and proved the basic properties._ Mon Sep 19 07:26:50 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-26-50-570951000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-26-50-570951000-PDT.html [nogin] Earlier today, a few .prla files got corrupted and three commits back I_ve_ Mon Sep 19 07:33:46 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-33-46-772999000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-33-46-772999000-PDT.html [nogin] A few fixes in the srec type._ Mon Sep 19 07:34:01 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-34-01-015647000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-34-01-015647000-PDT.html [kopylov] _Rename depth __ bdepth_ Mon Sep 19 07:34:04 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-34-04-361320000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-34-04-361320000-PDT.html [kopylov] More proofs_ Mon Sep 19 07:34:05 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-34-05-514605000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-34-05-514605000-PDT.html [kopylov] More proofs_ Mon Sep 19 07:34:20 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-34-20-215582000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-34-20-215582000-PDT.html [kopylov] more proofs_ Mon Sep 19 07:34:21 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-34-21-255052000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-34-21-255052000-PDT.html [kopylov] more proofs_ Mon Sep 19 07:34:23 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-34-23-031948000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-34-23-031948000-PDT.html [nogin] The scoping testing for conditional rewrites was doing a wrong thing for_ Mon Sep 19 07:34:24 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-34-24-085737000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-34-24-085737000-PDT.html [kopylov] Corrected some theorems_ Mon Sep 19 07:34:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-34-25-050971000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-34-25-050971000-PDT.html [kopylov] The rule tunionElimination_eq had unfinished proof. I removed it from the elimination resource. I added the rule tunionElimination_sq instead_ Mon Sep 19 07:34:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-34-25-488529000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-34-25-488529000-PDT.html [kopylov] more proofs_ Mon Sep 19 07:34:26 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-34-26-371461000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-34-26-371461000-PDT.html [kopylov] Finished proofs in itt_hoas_bterm_ Mon Sep 19 07:34:46 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-34-46-277126000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-34-46-277126000-PDT.html [nogin] Filled in a missing proof. Now all the Itt_hoas_bterm rules have fully_ Mon Sep 19 07:34:47 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-34-47-482790000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-34-47-482790000-PDT.html [nogin] Minor formatting fixes_ Mon Sep 19 07:34:50 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-34-50-478535000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2005-05/2005-09-19-07-34-50-478535000-PDT.html