[nogin] Reviwed ocaml_sos._ Mon Sep 19 02:50:47 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-50-47-389087000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-50-47-389087000-PDT.html [nogin] Eliminated some non_standard and unnecessary usage of slot___ Mon Sep 19 02:50:49 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-50-49-029440000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-50-49-029440000-PDT.html [nogin] Exposed the param_shape type that I need to add shapes to opname parsing._ Mon Sep 19 02:50:49 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-50-49-803927000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-50-49-803927000-PDT.html [yegor] 1.Some minor changes in old files_ Mon Sep 19 02:50:50 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-50-50-319030000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-50-50-319030000-PDT.html [yegor] Core of Arith _ search positive cycle in labelled graph._ Mon Sep 19 02:51:04 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-04-630851000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-04-630851000-PDT.html [yegor] Forgot to commit_ Mon Sep 19 02:51:05 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-05-294948000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-05-294948000-PDT.html [yegor] Forgot to checkin_ Mon Sep 19 02:51:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-07-022631000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-07-022631000-PDT.html [nogin] Eliminated more unnecessary usages of slot._ Mon Sep 19 02:51:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-07-466260000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-07-466260000-PDT.html [nogin] A few display form fixes._ Mon Sep 19 02:51:08 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-08-247760000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-08-247760000-PDT.html [nogin] _ Rformat now will use no more than 1/3 of the total width on the left tabs._ Mon Sep 19 02:51:10 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-10-038586000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-10-038586000-PDT.html [nogin] Check display forms at compile time._ Mon Sep 19 02:51:10 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-10-967188000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-10-967188000-PDT.html [nogin] Pass the _strictness_ flag to compile_contractum too, not just compile_redex._ Mon Sep 19 02:51:11 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-11-509265000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-11-509265000-PDT.html [nogin] _ Check the arity of the SO variables in the contractum at compile time._ Mon Sep 19 02:51:14 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-14-544239000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-14-544239000-PDT.html [nogin] _ Better error messages for typos in rules and rewrites._ Mon Sep 19 02:51:15 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-15-490830000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-15-490830000-PDT.html [nogin] The code responsible for computing extracts is completely broken _see BUGS 4.4_ Mon Sep 19 02:51:17 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-17-475435000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-17-475435000-PDT.html [nogin] I accidentally disabled the code that was creating display forms _ fixed._ Mon Sep 19 02:51:17 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-17-990865000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-17-990865000-PDT.html [nogin] Reverting the last change I did on dforms in this file _ that was a mistake._ Mon Sep 19 02:51:18 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-18-600351000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-18-600351000-PDT.html [nogin] Disallow changing parameter types in rewriter._ Mon Sep 19 02:51:20 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-20-697602000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-20-697602000-PDT.html [nogin] _ Fixed slot[_raw_, ...]_ Mon Sep 19 02:51:22 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-22-563217000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-22-563217000-PDT.html [nogin] Finally, I am able to commit what I was getting to_ Mon Sep 19 02:51:23 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-23-109994000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-23-109994000-PDT.html [nogin] Replaced the member operator with equal to match what we did for ITT_ Mon Sep 19 02:51:29 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-29-751215000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-29-751215000-PDT.html [nogin] TPTP_ added missing declarations._ Mon Sep 19 02:51:30 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-30-278177000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-30-278177000-PDT.html [nogin] _ Removed references to [un]fold_momber from FOL._ Mon Sep 19 02:51:31 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-31-797709000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-31-797709000-PDT.html [nogin] Cosmetic changes to avoid warnings with newer versions of GCC._ Mon Sep 19 02:51:35 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-35-982993000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-35-982993000-PDT.html [nogin] Minor tweaks._ Mon Sep 19 02:51:36 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-36-720287000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-36-720287000-PDT.html [nogin] Use Mozilla when available._ Mon Sep 19 02:51:38 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-38-676596000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-38-676596000-PDT.html [nogin] I joined Itt_hide and Itt_squash into a single theory _ Itt_squash that deals_ Mon Sep 19 02:51:39 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-39-219306000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-39-219306000-PDT.html [nogin] These are unused since May_99._ Mon Sep 19 02:51:47 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-47-458462000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-47-458462000-PDT.html [nogin] Exported locale_aware libc functions such as isdigit._ Mon Sep 19 02:51:48 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-48-881364000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-48-881364000-PDT.html [nogin] Display form fixes._ Mon Sep 19 02:51:51 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-51-101051000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-51-101051000-PDT.html [nogin] _ Proved all the theorems in itt_squash._ Mon Sep 19 02:51:53 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-53-251177000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-53-251177000-PDT.html [nogin] Fixed term __ AST conversion for array patterns._ Mon Sep 19 02:51:57 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-57-244002000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-57-244002000-PDT.html [nogin] I rewrote the Itt_squash tactics and the squash_resource implementation_ Mon Sep 19 02:51:57 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-57-754518000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-51-57-754518000-PDT.html [nogin] CZF_ renamed squash_related tactics, but haven_t checked that all proofs_ Mon Sep 19 02:53:31 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-53-31-949920000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-53-31-949920000-PDT.html [nogin] Use terminal width for output in a more consistent manner._ Mon Sep 19 02:53:33 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-53-33-421082000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2001-05/2005-09-19-02-53-33-421082000-PDT.html