[nogin] __0_ is a literal string _0_ to protect from spaces one needs to use double_Mon Sep 19 07:18:49 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-18-49-521413000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-18-49-521413000-PDT.html[nogin] Use Lm_symbol.compare instead of Pervasives.compare where appropriate._Mon Sep 19 07:18:55 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-18-55-100948000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-18-55-100948000-PDT.html[nogin] Got rid of .mlz in mllib and refiner directories._Mon Sep 19 07:18:55 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-18-55-458780000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-18-55-458780000-PDT.html[nogin] Removed an unused module._Mon Sep 19 07:18:56 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-18-56-050246000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-18-56-050246000-PDT.html[jyh] Added a line to term_base_ds to avoid the capture problem in bug _432._Mon Sep 19 07:18:58 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-18-58-796931000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-18-58-796931000-PDT.html[jyh] Added string lexing as a primitive to Filter_grammar._Mon Sep 19 07:19:00 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-00-422779000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-00-422779000-PDT.html[nogin] This augments the basic term type, adding support for the _shape_ parameters._Mon Sep 19 07:19:02 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-02-286854000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-02-286854000-PDT.html[jyh] Incomplete support for strings in the backend._Mon Sep 19 07:19:05 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-05-219472000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-05-219472000-PDT.html[nogin] Made term_std_s standardize function closer to term_ds_s one._Mon Sep 19 07:19:05 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-05-836202000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-05-836202000-PDT.html[jyh] Added explicit iform category for terms. The syntax is__Mon Sep 19 07:19:07 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-07-201321000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-07-201321000-PDT.html[jyh] Ignore quoted terms during checking._Mon Sep 19 07:19:10 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-10-399276000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-10-399276000-PDT.html[nogin] WARNING_ Jason_s earlier commit broke binary compatibility_ this one makes it_Mon Sep 19 07:19:10 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-10-778886000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-10-778886000-PDT.html[nogin] In ITT, annotated the iform opnames with _declare iform__Mon Sep 19 07:19:11 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-12-001493000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-12-001493000-PDT.html[jyh] In iform checking, handle quoted shapes by stripping the quotes._Mon Sep 19 07:19:12 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-12-619969000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-12-619969000-PDT.html[nogin] Updated display forms for the _declare_ directives to match the current term_Mon Sep 19 07:19:13 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-13-741744000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-13-741744000-PDT.html[nogin] Updated refiner_debug._Mon Sep 19 07:19:14 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-14-193576000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-14-193576000-PDT.html[jyh] Removed the _ignore check in input term checking. I had forgotten_Mon Sep 19 07:19:15 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-15-157083000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-15-157083000-PDT.html[nogin] _define iform_ will now correctly create an iform, not a rewrite._Mon Sep 19 07:19:16 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-16-597203000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-16-597203000-PDT.html[jyh] Added a little better error messages to the unifier._Mon Sep 19 07:19:22 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-22-797472000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-22-797472000-PDT.html[jyh] Minor cleanups. Aleksey found the problem with type inference, we_Mon Sep 19 07:19:23 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-23-263215000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-23-263215000-PDT.html[xiny] Changed the way to interpreting op_bdepth and variablesin Itt_reflection_new._Mon Sep 19 07:19:27 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-27-541297000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-27-541297000-PDT.html[xiny] Changed comments with _fake_mlrw_._Mon Sep 19 07:19:28 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-28-376448000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-28-376448000-PDT.html[kopylov] Fixed a definition of beta_redex_Mon Sep 19 07:19:28 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-28-823051000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-28-823051000-PDT.html[nogin] _ When displaying slot[_raw_,_s_], the string _s_ _must_ really be displayed_Mon Sep 19 07:19:29 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-29-229911000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-29-229911000-PDT.html[nogin] Simplified the rlist code_Mon Sep 19 07:19:29 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-29-708919000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-29-708919000-PDT.html[nogin] More precise meta_typing for the qouted terms._Mon Sep 19 07:19:30 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-30-101970000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-30-101970000-PDT.html[nogin] Rudimentary support for displaying shapes_Mon Sep 19 07:19:30 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-30-584871000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-30-584871000-PDT.html[nogin] In table_based tactics and conversions, call the get_resource_arg once in the_Mon Sep 19 07:19:31 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-31-117685000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-31-117685000-PDT.html[nogin] Killed a leftover MLZFILES definition._Mon Sep 19 07:19:33 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-33-224507000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-33-224507000-PDT.html[nogin] Updated the _You need OMake_ error message._Mon Sep 19 07:19:33 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-33-631084000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-33-631084000-PDT.html[nogin] With TERMS_std, we were getting an _illegal subterm Perv_concl_...__ error_Mon Sep 19 07:19:34 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-34-043861000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-34-043861000-PDT.html[jyh] This is the bare template for pmc, which is completely empty right_Mon Sep 19 07:19:37 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-37-625889000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-37-625889000-PDT.html[jyh] Move the config to the compiler_specific directories._Mon Sep 19 07:19:40 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-40-590244000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-40-590244000-PDT.html[jyh] Remove mmc configuration._Mon Sep 19 07:19:49 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-49-145111000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-19-49-145111000-PDT.html[nogin] Added meta_eq[sh, sh]_Mon Sep 19 07:20:01 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-01-945276000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-01-945276000-PDT.html[nogin] In messages that say that a config file was created/updated, give the full_Mon Sep 19 07:20:04 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-04-101665000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-04-101665000-PDT.html[jyh] Letting the paper cook for a while._Mon Sep 19 07:20:14 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-14-607650000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-14-607650000-PDT.html[yegor] replaced applHLeft with prodApp _which is a combination of prodH and application__Mon Sep 19 07:20:15 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-15-236687000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-15-236687000-PDT.html[yegor] I think, I fixed the Dep rule by switching from generic ForAll1T1DT to a_Mon Sep 19 07:20:17 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-17-029416000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-17-029416000-PDT.html[nogin] As far as I understand, type_subst v t TypeExists_v_, ..._ was not handling_Mon Sep 19 07:20:22 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-22-824758000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-22-824758000-PDT.html[yegor] Commiting some experimental proofs before bringing up_to_date local metaprl tree._Mon Sep 19 07:20:28 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-28-287809000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-28-287809000-PDT.html[nogin] Allow intro resource annotations of the form_Mon Sep 19 07:20:31 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-31-281845000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-31-281845000-PDT.html[nogin] A better _precedence not found_ error message._Mon Sep 19 07:20:36 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-36-148566000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-36-148566000-PDT.html[nogin] Print an error message when trying to compile a MetaPRL file that has a .ml,_Mon Sep 19 07:20:37 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-37-394118000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-37-394118000-PDT.html[nogin] Created a typeclass MTerm for meta_terms and changed the_Mon Sep 19 07:20:44 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-44-822956000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-44-822956000-PDT.html[nogin] Added slot[_esc_, s_s] and slot[_cesc_, s_s] display forms for printing the_Mon Sep 19 07:20:45 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-45-539803000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-45-539803000-PDT.html[jyh] Updated Filter_grammar to match the Lm_lexer change from omake._Mon Sep 19 07:20:46 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-46-208408000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-46-208408000-PDT.html[jyh] Oops, I was confused. MetaPRL requires the newest version of Lm_lexer,_Mon Sep 19 07:20:46 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-46-917726000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-46-917726000-PDT.html[jyh] The magic numbers are now compatible across omake versions._Mon Sep 19 07:20:47 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-47-280002000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-47-280002000-PDT.html[jyh] Added a blank line._Mon Sep 19 07:20:47 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-47-645122000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-47-645122000-PDT.html[jyh] Rename the _string_ extension to _str_, to avoid confusion with_Mon Sep 19 07:20:49 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-49-512191000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-49-512191000-PDT.html[nogin] Reverting the magic number to the Unix one._Mon Sep 19 07:20:50 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-50-078576000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-50-078576000-PDT.html[yegor] Some fixes and improvements in cic_ind_elim__Mon Sep 19 07:20:51 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-51-371297000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-51-371297000-PDT.html[yegor] More fixes, still incomplete_Mon Sep 19 07:20:52 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-52-194707000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-52-194707000-PDT.html[nogin] Added a comment_Mon Sep 19 07:20:53 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-53-300499000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-53-300499000-PDT.html[jyh] Added to the exceptions chapter._Mon Sep 19 07:20:53 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-53-698181000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-53-698181000-PDT.html[yegor] Old proofs are up_to_date now._Mon Sep 19 07:20:54 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-54-509871000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-54-509871000-PDT.html[jyh] Working on outstanding issues for Win32._Mon Sep 19 07:20:55 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-55-427398000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-55-427398000-PDT.html[yegor] It_s almost working. We have two problems__Mon Sep 19 07:20:56 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-56-099845000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-56-099845000-PDT.html[yegor] Forgot proofs_Mon Sep 19 07:20:56 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-56-727925000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2005-04/2005-09-19-07-20-56-727925000-PDT.html