Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-08-06 17:06:32 -0700 (Fri, 06 Aug 2004)
Revision: 6115
Log message:

      Improved warning message when a grammar has conflicts.  "There were errors" is
      not the most helpful message IMHO.
      
      Also augmented parser to accept sequents with anonymous hypotheses.  For
      example:    sequent{ foo{}; bar{}; x:baz{} >- nil{} }
      

Changes by: ( at unknown.email)
Date: 2004-08-06 17:06:32 -0700 (Fri, 06 Aug 2004)
Revision: 6116
Log message:

      This commit was manufactured by cvs2svn to create branch 'shell_begin'.

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-08-11 16:24:14 -0700 (Wed, 11 Aug 2004)
Revision: 6118
Log message:

      Correcting the parsing of anonymous hypotheses.  I was making up a variable
      instead of using Lm_symbol.empty_var as the variable bound to an anonymous
      hypothesis.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-08-19 22:41:44 -0700 (Thu, 19 Aug 2004)
Revision: 6124
Log message:

      MP_DIRS needs to be an array in the first place; fixing it later with a split
      is a bad idea since this causes the effects of $(dir ...) to be lost (which
      was why the editor/ml/tests directory could not be compiled).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-08-20 17:58:22 -0700 (Fri, 20 Aug 2004)
Revision: 6125
Log message:

      Allow "smart" syntax in non-binding hypotheses. Fixes bug 273.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-08-21 18:32:16 -0700 (Sat, 21 Aug 2004)
Revision: 6126
Log message:

      Not sure whether we need filter_bin or not, but made sure it still compiles -
      just in case we do.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-08-23 16:41:50 -0700 (Mon, 23 Aug 2004)
Revision: 6127
Log message:

       - Added display forms for bterms.
       - Added the simple-bterm case for "dest_bterm" (Note: Alexei suggested
         to rename "dest_bterm" as "subterms_of_bterm" or just "subterms",
         because it only gives us subterms.)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-08-24 18:35:26 -0700 (Tue, 24 Aug 2004)
Revision: 6131
Log message:

      Fixing the TEXINPUTS.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-08-24 19:46:54 -0700 (Tue, 24 Aug 2004)
Revision: 6132
Log message:

      - Made sure that theories.pdf compiles.
      - There were two copies of book2.tex, removing the unused one.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-08-24 20:08:59 -0700 (Tue, 24 Aug 2004)
Revision: 6133
Log message:

      - Added a simple framework for annotating refiner error messages with
        better explanaitions. For now, only RewriteFreeSOVar is annotated.
      - Very minor code simplification in lm_rformat
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-08-25 00:23:01 -0700 (Wed, 25 Aug 2004)
Revision: 6134
Log message:

      Added reflection in Itt. The induction on bterm is not implemented yet.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-08-25 11:45:04 -0700 (Wed, 25 Aug 2004)
Revision: 6135
Log message:

      Adding one of the TPHOLs cat B papers and the PS/PDF for the resources paper.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-08-25 13:00:15 -0700 (Wed, 25 Aug 2004)
Revision: 6136
Log message:

      By default, build ocaml book without MathTimes fonts (this uses book2.tex).
      For MathTimes, use "omake jyh_doc" or "omake jyh_tex" (this uses book3.tex).
      
      Once bug 267 RFE is implemented, we should be able to toggle this in a less
      ad-hoc manner.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-08-25 19:25:35 -0700 (Wed, 25 Aug 2004)
Revision: 6137
Log message:

      Trivial simplification of the code.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-08-25 21:48:25 -0700 (Wed, 25 Aug 2004)
Revision: 6139
Log message:

      - Adjusted the precedences so that the "smart" syntax for sequents is parsed
      correctly. E.g. "a b{| ... |}" is now correctly parsed as "a ('b{| ... |})"
      instead of "(a b){| ... |}" and similarly for "a in b{| ... |}" and other
      operators.
      - Simplified the grammar a bit, removing some unnecessary restrictions (for
      example, the notion of "applyterm" was removed - now any term not containing
      a non-parenticized coma can be a subterm of an application).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-08-25 22:35:52 -0700 (Wed, 25 Aug 2004)
Revision: 6140
Log message:

      Beofre displaying a term, convert every Context in it into a Hypothesis.
      (<H...> would become df_context{'H...} with H becoming a second-order
      variable with the same context dependencies and subterms as the original context).
      Basically, this means that we have one centralized "standard" hack for contexts
      as opposed to having to reimplement it in every theory that wants non-default
      display forms for sequents.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-08-26 18:35:32 -0700 (Thu, 26 Aug 2004)
Revision: 6142
Log message:

      This is a branch to bring metaprl in line with the omake branch.
      98% of these changes are just to .cvsignore files, which should
      ignore .omc and .omo generated files.
      
      There are a few changes to OMakefiles.  This is because
      the $'(...) sequence has been replaced by $`(...).
      $'a b c' is now symmetric with $"a b c", as a quotation.
      $'...' does not expand variables in the quotation, $"..." does.
      
      This will probably be a very short-lived branch...
      We can remove the tag later if this is a problem.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-08-27 20:23:35 -0700 (Fri, 27 Aug 2004)
Revision: 6146
Log message:

      More .cvsignore changes.
      I should have committed the book changes to the trunk....
      Well, this brings MetaPRL in line with the latest omake changes.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-08-27 20:35:06 -0700 (Fri, 27 Aug 2004)
Revision: 6147
Log message:

      More .cvsignore changes.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-08-29 19:09:44 -0700 (Sun, 29 Aug 2004)
Revision: 6148
Log message:

      Merged the shell_begin branch.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-08-29 20:18:48 -0700 (Sun, 29 Aug 2004)
Revision: 6149
Log message:

      As a workaround for bug 287 (hopefully, a temporary one), I put OMakeVersion into
      OMakeroot as well.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-08-30 08:42:40 -0700 (Mon, 30 Aug 2004)
Revision: 6150
Log message:

      Use add-wrapper, not add-quoted-wrapper.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-08-30 13:20:35 -0700 (Mon, 30 Aug 2004)
Revision: 6151
Log message:

      More changes to the book.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-08-31 17:21:49 -0700 (Tue, 31 Aug 2004)
Revision: 6152
Log message:

      Added explanation to AllSOInstances error.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-08-31 17:50:30 -0700 (Tue, 31 Aug 2004)
Revision: 6153
Log message:

      In responce to Nathan's troubles, making the parsing of contexts more liberal:
      - Allow "[]" in 0 arity contexts
      - Allow "<||>" (in addition to "<| |>") the same way as it is allowed for SO
      variables.