Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-03 16:18:38 -0700 (Thu, 03 Jul 2003)
Revision: 4693
Log message:

      Added some example code for how we want new term
      constructors and destructors in core_type_infer.ml.
      This code doesn't compile, but it demonstrates the
      concept.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-03 16:19:36 -0700 (Thu, 03 Jul 2003)
Revision: 4694
Log message:

      Forgot to add the file.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-03 20:56:03 -0700 (Thu, 03 Jul 2003)
Revision: 4697
Log message:

      Beginning the slow process of migrating MetaPRL toward libmojave.
      

Changes by: ( at unknown.email)
Date: 2003-07-04 13:52:30 -0700 (Fri, 04 Jul 2003)
Revision: 4700
Log message:

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

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-06 16:41:01 -0700 (Sun, 06 Jul 2003)
Revision: 4704
Log message:

      I decided to finish the port to abstract vars anyway.
      
      This versdion compiles with omake.  Will fix make next.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-06 21:11:26 -0700 (Sun, 06 Jul 2003)
Revision: 4706
Log message:

      Migrated String_util and Mp_debug to libmojave versions.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-09 00:20:04 -0700 (Wed, 09 Jul 2003)
Revision: 4723
Log message:

      Merging in the abstract_vars branch:
      - variables are now an abstract type, not strings
      - MVar parameters are gone
      
      See the branch log messages for more information.
      
      P.S. This is a pretty big change, so I bumped the version number
      in mk/preface.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-11 15:34:52 -0700 (Fri, 11 Jul 2003)
Revision: 4731
Log message:

      Added a little more code for type inference.  The current
      code does not handle bounded quantifiers correctly.
      

Changes by: ( at unknown.email)
Date: 2003-07-13 03:34:55 -0700 (Sun, 13 Jul 2003)
Revision: 4736
Log message:

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

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-13 18:39:54 -0700 (Sun, 13 Jul 2003)
Revision: 4738
Log message:

      Core_type_infer now compiles, though completely untested.
      Fixed a dumb dependency bug in OMakefile.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-14 11:00:00 -0700 (Mon, 14 Jul 2003)
Revision: 4739
Log message:

      Some minor changes.
      
      Did not change Term_match_table.  We'll have to decide if we
      want default cases.
      
      Core_type_erase also has an issue with default cases.
      Specifically, all types are erased, but all variables
      are left wrapped, like erase{'v}.  I'm not sure we want
      to add a default case.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-14 11:00:22 -0700 (Mon, 14 Jul 2003)
Revision: 4740
Log message:

      Forgot to add this file.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-15 17:07:35 -0700 (Tue, 15 Jul 2003)
Revision: 4749
Log message:

      Merged CPS conversion and sequent representation of
      quantifiers onto the trunk.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-18 19:29:12 -0700 (Fri, 18 Jul 2003)
Revision: 4761
Log message:

      Added sequents to <:con< ... >> quotation.
      Here's a short summary of syntax:
      
         e ::= sequent [args] { hyps >- con_term list }
         args ::= con_term list  -- The usual syntax for these terms
         hyp ::= <H> | <H[con_terms]>
             |   <$e$>           -- $e$ should be a list of hypothesis terms
             |   v:con_term
             |   $v$:con_term
      
      This is the first pass, undoubtly we'll need some tuning.
      

Changes by: ( at unknown.email)
Date: 2003-07-23 14:40:47 -0700 (Wed, 23 Jul 2003)
Revision: 4768
Log message:

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

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2003-07-23 14:40:47 -0700 (Wed, 23 Jul 2003)
Revision: 4769
Log message:

      Added sequents code to all the files...
      

Changes by: ( at unknown.email)
Date: 2003-07-28 17:33:02 -0700 (Mon, 28 Jul 2003)
Revision: 4782
Log message:

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