Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-04 13:34:06 -0700 (Mon, 04 Aug 2003)
Revision: 4813
Log message:

      The new explicit-contexts code discovered a bug, now we have to
      figure out how to fix it.
      
      Consider the following rewrite, which is obviously sensible.
      
         Lambda{x. 'e['x]} : TyAll{y. 't['y]}
         <-->
         Lambda{x. TyConstrain{'e['x]; 't['x]}} : TyAll{y. 't['y]}
      
      Now consider the sequent form, which does something similar,
      but fails because of the context substitution.
      
         sequent [Lambda] { <H> >- 'e } : sequent [TyAll] { <K> >- 't<|K|> }
         <-->
         sequent [Lambda] { <H> >- TyConstrain{'e; 't<|H|>} } :
         sequent [TyAll] { <H> >- 't<|K|> }
      

Changes  Path
+9 -3 metaprl/OMakefile
+1 -0 metaprl/clib/OMakefile
+1 -1 metaprl/doc/latex/theories/m-paper.tex
+8 -1 metaprl/filter/filter/filter_main.ml
+17 -5 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_ast.ml
+33 -16 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_cps.ml
+5 -1 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_tast.ml
+36 -42 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_type_check.ml