[n8gray] Improved warning message when a grammar has conflicts. _There were errors_ is_ Mon Sep 19 06:31:29 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-29-267477000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-29-267477000-PDT.html [] This commit was manufactured by cvs2svn to create branch _shell_begin_._ Mon Sep 19 06:31:29 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-29-740258000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-29-740258000-PDT.html [n8gray] Correcting the parsing of anonymous hypotheses. I was making up a variable_ Mon Sep 19 06:31:45 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-45-600187000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-45-600187000-PDT.html [nogin] MP_DIRS needs to be an array in the first place_ fixing it later with a split_ Mon Sep 19 06:31:48 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-48-816332000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-48-816332000-PDT.html [nogin] Allow _smart_ syntax in non_binding hypotheses. Fixes bug 273._ Mon Sep 19 06:31:49 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-49-217337000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-49-217337000-PDT.html [nogin] Not sure whether we need filter_bin or not, but made sure it still compiles __ Mon Sep 19 06:31:49 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-49-623900000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-49-623900000-PDT.html [xiny] _ Added display forms for bterms._ Mon Sep 19 06:31:50 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-50-021205000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-50-021205000-PDT.html [nogin] Fixing the TEXINPUTS._ Mon Sep 19 06:31:52 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-52-251426000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-52-251426000-PDT.html [nogin] _ Made sure that theories.pdf compiles._ Mon Sep 19 06:31:52 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-52-628687000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-52-628687000-PDT.html [nogin] _ Added a simple framework for annotating refiner error messages with_ Mon Sep 19 06:31:53 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-53-132520000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-53-132520000-PDT.html [xiny] Added reflection in Itt. The induction on bterm is not implemented yet._ Mon Sep 19 06:31:53 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-53-515755000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-53-515755000-PDT.html [nogin] Adding one of the TPHOLs cat B papers and the PS/PDF for the resources paper._ Mon Sep 19 06:31:55 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-55-711479000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-55-711479000-PDT.html [nogin] By default, build ocaml book without MathTimes fonts _this uses book2.tex_._ Mon Sep 19 06:31:56 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-56-134979000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-56-134979000-PDT.html [nogin] Trivial simplification of the code._ Mon Sep 19 06:31:56 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-56-560189000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-56-560189000-PDT.html [nogin] _ Adjusted the precedences so that the _smart_ syntax for sequents is parsed_ Mon Sep 19 06:31:57 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-57-497035000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-57-497035000-PDT.html [nogin] Beofre displaying a term, convert every Context in it into a Hypothesis._ Mon Sep 19 06:31:58 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-58-137957000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-58-137957000-PDT.html [jyh] This is a branch to bring metaprl in line with the omake branch._ Mon Sep 19 06:31:59 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-59-198087000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-31-59-198087000-PDT.html [jyh] More .cvsignore changes._ Mon Sep 19 06:32:03 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-32-03-711035000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-32-03-711035000-PDT.html [jyh] More .cvsignore changes._ Mon Sep 19 06:32:06 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-32-06-644897000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-32-06-644897000-PDT.html [jyh] Merged the shell_begin branch._ Mon Sep 19 06:32:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-32-07-419244000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-32-07-419244000-PDT.html [nogin] As a workaround for bug 287 _hopefully, a temporary one_, I put OMakeVersion into_ Mon Sep 19 06:32:10 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-32-10-574170000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-32-10-574170000-PDT.html [jyh] Use add_wrapper, not add_quoted_wrapper._ Mon Sep 19 06:32:10 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-32-10-930879000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-32-10-930879000-PDT.html [jyh] More changes to the book._ Mon Sep 19 06:32:11 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-32-11-302185000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-32-11-302185000-PDT.html [nogin] Added explanation to AllSOInstances error._ Mon Sep 19 06:32:12 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-32-12-119660000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-32-12-119660000-PDT.html [nogin] In responce to Nathan_s troubles, making the parsing of contexts more liberal__ Mon Sep 19 06:32:12 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-32-12-499462000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2004-08/2005-09-19-06-32-12-499462000-PDT.html