[nogin] Do not use ocamlfind, even if it is installed._ Mon Sep 19 06:34:51 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-34-51-770742000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-34-51-770742000-PDT.html [yegor] New code that generates trace of supinf_s reasoning and than constructs the proof._ Mon Sep 19 06:34:52 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-34-52-174972000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-34-52-174972000-PDT.html [yegor] My previous commit introduced a bug in SupInf which was causing _wrong_ results in_ Mon Sep 19 06:34:53 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-34-53-619646000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-34-53-619646000-PDT.html [kopylov] Define a type for simple lambda terms._ Mon Sep 19 06:34:54 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-34-54-126172000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-34-54-126172000-PDT.html [yegor] Forgot to switch off the debug output_ Mon Sep 19 06:35:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-35-07-109638000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-35-07-109638000-PDT.html [nogin] The Smap module was just a dup of Lm_serial_map._ Mon Sep 19 06:35:09 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-35-09-272955000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-35-09-272955000-PDT.html [nogin] The CVS version of OCaml now supports _unused variable_ warnings._ Mon Sep 19 06:35:09 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-35-09-843269000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-35-09-843269000-PDT.html [nogin] Committed a bit too much in my last commit._ Mon Sep 19 06:35:10 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-35-10-598077000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-35-10-598077000-PDT.html [nogin] Fixing another breakage from yesterday_s commit. Sorry for not fixing it earlier._ Mon Sep 19 06:35:10 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-35-10-978251000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-35-10-978251000-PDT.html [nogin] In automated scripts, unset OMAKEFLAGS before running omake._ Mon Sep 19 06:35:11 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-35-11-600415000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-35-11-600415000-PDT.html [yegor] Finally, I_ve managed to export most of the proofs._ Mon Sep 19 06:35:12 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-35-12-101395000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-35-12-101395000-PDT.html [yegor] A little more proofs._ Mon Sep 19 06:42:33 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-42-33-567147000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-42-33-567147000-PDT.html [nogin] Updating some of the autoT stuff to fix some of the proofs broken by_ Mon Sep 19 06:42:36 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-42-36-725650000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-42-36-725650000-PDT.html [nogin] More unused variables eliminated._ Mon Sep 19 06:42:38 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-42-38-851659000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-42-38-851659000-PDT.html [nogin] Split couple of long lines._ Mon Sep 19 06:42:39 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-42-39-921545000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-42-39-921545000-PDT.html [nogin] Chages and comments from today_s reflection meeting _I haven_t yet made any_ Mon Sep 19 06:42:40 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-42-40-324006000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-42-40-324006000-PDT.html [nogin] Fixing some of the proofs broken by today_s reflection changes._ Mon Sep 19 06:42:41 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-42-41-222638000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-42-41-222638000-PDT.html [yegor] Moved some code from itt_supinf to reflib/supinf_ Mon Sep 19 06:42:49 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-42-49-997876000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-42-49-997876000-PDT.html [nogin] Fixed _omake doc_._ Mon Sep 19 06:42:51 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-42-51-468365000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-42-51-468365000-PDT.html [nogin] Do not use _file_line_error_style yet._ Mon Sep 19 06:42:52 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-42-52-034017000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-42-52-034017000-PDT.html [yegor] itt_rat _ definition of GCD was incorrect on negative numbers_ Mon Sep 19 06:42:52 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-42-52-394216000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-42-52-394216000-PDT.html [yegor] Now it does not normalize hypotheses that are not used._ Mon Sep 19 06:42:53 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-42-53-791640000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-42-53-791640000-PDT.html [nogin] MetaPRL works fine with 3.08.2 _no special patches needed_._ Mon Sep 19 06:42:56 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-42-56-518721000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-42-56-518721000-PDT.html [nogin] Xstr_search was borrowed from somebody else_s package and I am unsure_ Mon Sep 19 06:42:58 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-42-58-636700000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-42-58-636700000-PDT.html [yegor] _is_empty_ added to the interface_ Mon Sep 19 06:42:59 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-42-59-269850000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-42-59-269850000-PDT.html [yegor] 1. Fixed two bugs in old code _since spring__ Mon Sep 19 06:42:59 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-42-59-724832000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-42-59-724832000-PDT.html [yegor] Forgot to uncomment one little bit of code._ Mon Sep 19 06:43:00 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-43-00-483203000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-43-00-483203000-PDT.html [yegor] Now it understands that there is no integers between _n and _n_1_ Mon Sep 19 06:43:00 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-43-00-882631000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-11/2005-09-19-06-43-00-882631000-PDT.html