[jyh] Some corrections on file dependencies._ Mon Sep 19 06:18:48 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-18-48-318425000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-18-48-318425000-PDT.html [jyh] Add a _View_ window to control what is displayed in the browser._ Mon Sep 19 06:18:50 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-18-50-163188000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-18-50-163188000-PDT.html [jyh] o Added term _handles_ in browser mode. These allow more precise_ Mon Sep 19 06:18:50 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-18-50-995492000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-18-50-995492000-PDT.html [jyh] In HTML mode_ the status line should give _relative_ links._ Mon Sep 19 06:18:52 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-18-52-426874000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-18-52-426874000-PDT.html [nogin] Fixing bug 219_ only compute the _address array index_ of a hyp context,_ Mon Sep 19 06:18:53 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-18-53-272367000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-18-53-272367000-PDT.html [natasha] Started to work on case analysis operation for inductively defined types_ Mon Sep 19 06:18:53 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-18-53-650457000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-18-53-650457000-PDT.html [natasha] 1. some fixes in cic_lambda _got rid of WF_context_ __ Mon Sep 19 06:18:54 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-18-54-239208000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-18-54-239208000-PDT.html [emre] itt_list2_ exposing rev__l_ so that it can be used in other modules_ Mon Sep 19 06:18:55 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-18-55-909915000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-18-55-909915000-PDT.html [yegor] unistd.h is not present in under win32 so it should not be included there_ Mon Sep 19 06:20:22 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-20-22-918240000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-20-22-918240000-PDT.html [yegor] term_op _ dep0_dep0_dep2 operations added to support induction over naturals_ Mon Sep 19 06:20:23 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-20-23-273721000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-20-23-273721000-PDT.html [yegor] I started the theory of multivariate _or multivariable__ polynomials on top of_ Mon Sep 19 06:20:23 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-20-23-902922000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-20-23-902922000-PDT.html [yegor] next step to normalization__ Mon Sep 19 06:20:26 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-20-26-809336000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-20-26-809336000-PDT.html [n8gray] Allow user to override font and bold color with env. vars MPFONT and MPBOLD._ Mon Sep 19 06:20:35 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-20-35-162050000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-20-35-162050000-PDT.html [yegor] added Z.1 and Z.eq so Z is actually in unitringCE_ Mon Sep 19 06:20:36 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-20-36-285136000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-20-36-285136000-PDT.html [nogin] Removing unused code _it was a part of the old_style comments support_._ Mon Sep 19 06:20:36 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-20-36-670376000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-20-36-670376000-PDT.html [yegor] list2 _ added standard helpers for length__ like mk_length_term, etc_ Mon Sep 19 06:20:42 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-20-42-197873000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-20-42-197873000-PDT.html [yegor] normalization is kind of work but really slow _ 10 secs for_ Mon Sep 19 06:20:42 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-20-42-691107000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-20-42-691107000-PDT.html [yegor] I_m trying another approach to multivariate polynomials__ Mon Sep 19 06:21:31 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-21-31-182248000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-21-31-182248000-PDT.html [yegor] removed timingT_ Mon Sep 19 06:21:33 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-21-33-439891000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-21-33-439891000-PDT.html [nogin] Moved the param_ type to the top_level of the Term_sig module_ Mon Sep 19 06:21:34 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-21-34-287553000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-21-34-287553000-PDT.html [nogin] Use dest_params instead of _List.map dest_param_ and similar constructs._ Mon Sep 19 06:21:35 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-21-35-853900000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-21-35-853900000-PDT.html [yegor] Polynomial normalization works fine,_ Mon Sep 19 06:21:36 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-21-36-931838000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-21-36-931838000-PDT.html [yegor] makefiles _ removed references to itt_mpoly_ Mon Sep 19 06:21:46 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-21-46-442830000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-21-46-442830000-PDT.html [nogin] A bit more profiling support. Now to get the profile text, one only needs to_ Mon Sep 19 06:21:59 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-21-59-346269000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-21-59-346269000-PDT.html [nogin] Minor code clean_up _should also speed up things a little_._ Mon Sep 19 06:21:59 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-21-59-751110000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-21-59-751110000-PDT.html [nogin] Minor code cleanup._ Mon Sep 19 06:22:01 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-22-01-102347000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-22-01-102347000-PDT.html [nogin] Minor clean_up._ Mon Sep 19 06:22:01 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-22-01-790469000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-22-01-790469000-PDT.html [yegor] Tiny adjustments_ Mon Sep 19 06:22:02 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-22-02-170349000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-22-02-170349000-PDT.html [nogin] Removing couple of unused types._ Mon Sep 19 06:22:02 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-22-02-712419000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-22-02-712419000-PDT.html [yegor] Made a benchmarking__ Mon Sep 19 06:22:03 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-22-03-104133000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-22-03-104133000-PDT.html [yegor] Infinite cycle was due to a rule added to elim_resource that can be_ Mon Sep 19 06:22:24 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-22-24-116824000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-22-24-116824000-PDT.html [nogin] Comented out the _crwhigher_ refiner mechanism. The tactics module will now_ Mon Sep 19 06:22:41 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-22-41-842484000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-22-41-842484000-PDT.html [nogin] Simplified the internal address type in Term_ds. The Term_std could probably be_ Mon Sep 19 06:22:42 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-22-42-443932000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-22-42-443932000-PDT.html [nogin] Oops, forgot the .mli change in the last commit._ Mon Sep 19 06:22:42 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-22-43-004310000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-22-43-004310000-PDT.html [nogin] Fixed the out_of_scope test for assumptions produced by the conditional_ Mon Sep 19 06:22:43 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-22-43-384876000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-22-43-384876000-PDT.html [yegor] A fix to one of two proofs broken yesterday._ Mon Sep 19 06:22:43 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-22-43-991279000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-22-43-991279000-PDT.html [yegor] This repairs the second of two proofs broken yesterday._ Mon Sep 19 06:22:45 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-22-45-856749000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-22-45-856749000-PDT.html [nogin] Added stricter checking of the shapes for opnames specified using the FQN notation._ Mon Sep 19 06:22:56 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-22-56-699020000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-22-56-699020000-PDT.html [] This commit was manufactured by cvs2svn to create branch _quote_param_._ Mon Sep 19 06:22:57 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-22-57-155267000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-22-57-155267000-PDT.html [nogin] Adding the Quote parameter to the list of the possible term paramaters._ Mon Sep 19 06:23:12 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-12-872174000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-12-872174000-PDT.html [yegor] Split all evaluations to a separate resource, for now it refers to_ Mon Sep 19 06:23:13 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-13-375496000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-13-375496000-PDT.html [yegor] Tiny bugfix_ reduce_cmp_lexi had incorrect base case._ Mon Sep 19 06:23:13 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-13-873937000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-13-873937000-PDT.html [nogin] Give a better error message in interface/implementation mismatch._ Mon Sep 19 06:23:14 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-14-257922000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-14-257922000-PDT.html [yegor] list2 _ unfold_mklist was not in the interface_ Mon Sep 19 06:23:14 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-14-692696000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-14-692696000-PDT.html [nogin] Use an explicit MLast.loc type _as opposed to expanding it into _int _ int___ Mon Sep 19 06:23:15 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-15-404865000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-15-404865000-PDT.html [nogin] Use a _canonical_ Filter_util.dummy_loc instead of using __0, 0__ all over_ Mon Sep 19 06:23:15 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-15-983403000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-15-983403000-PDT.html [nogin] Removing an unused file._ Mon Sep 19 06:23:16 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-16-680720000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-16-680720000-PDT.html [nogin] One more place where MLast.loc should be used instead of int _ int_ Mon Sep 19 06:23:17 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-17-323681000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-17-323681000-PDT.html [nogin] Minor code cleanup/optimization._ Mon Sep 19 06:23:17 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-17-706267000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-17-706267000-PDT.html [jyh] This is the browser update I_ve been putting off._ Mon Sep 19 06:23:18 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-18-398017000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-18-398017000-PDT.html [nogin] More code clean_up._ Mon Sep 19 06:23:21 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-21-847826000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-21-847826000-PDT.html [jyh] SSL should be off by default._ Mon Sep 19 06:23:22 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-22-732963000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-22-732963000-PDT.html [nogin] The generated proxyedit_lex.ml should be ignored and cleaned._ Mon Sep 19 06:23:23 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-23-121316000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-23-121316000-PDT.html [nogin] Delete lib/_.gif and lib/_.pem on _omake clean__ Mon Sep 19 06:23:23 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-23-493958000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-23-493958000-PDT.html [nogin] More code clean_up. This speeds up _status_all_ by about 1_._ Mon Sep 19 06:23:23 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-23-868155000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-23-868155000-PDT.html [jyh] Win32 bugfix update. MetaPRL should now compile correctly on win32._ Mon Sep 19 06:23:24 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-24-487371000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-24-487371000-PDT.html [nogin] More clean_up._ Mon Sep 19 06:23:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-25-113255000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-25-113255000-PDT.html [xiny] Updated the refiner directory with the quote parameter._ Mon Sep 19 06:23:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-25-708267000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-25-708267000-PDT.html [jyh] New SSL method to provide a _standard_ socket interface,_ Mon Sep 19 06:23:26 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-26-699922000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-26-699922000-PDT.html [jyh] Proxyedit now works on win32, so we can call an external editor on windows._ Mon Sep 19 06:23:27 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-27-661216000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-27-661216000-PDT.html [nogin] More code clean_up._ Mon Sep 19 06:23:28 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-28-122510000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-28-122510000-PDT.html [nogin] _ in unquote_term, make sure term does not have one of the _special_ _var or_ Mon Sep 19 06:23:28 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-28-706958000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-28-706958000-PDT.html [jyh] Added some additional functions. Status_ tested with and without SSL on_ Mon Sep 19 06:23:29 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-29-189659000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-29-189659000-PDT.html [jyh] Minor changes to get Win32 to run._ Mon Sep 19 06:23:30 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-30-838836000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-30-838836000-PDT.html [jyh] Ignore more files._ Mon Sep 19 06:23:31 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-31-321695000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-31-321695000-PDT.html [jyh] Minor fixes._ Mon Sep 19 06:23:31 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-31-668575000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-23-31-668575000-PDT.html [emre] Itt_list2_ filled in a few proofs._ Mon Sep 19 06:24:10 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-24-10-170117000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-05/2005-09-19-06-24-10-170117000-PDT.html