Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-24 22:55:29 -0800 (Mon, 24 Jan 2005)
Revision: 6500
Log message:
Upgrading mmc.
Currently in Mmc_core_type_check.
Judgments like the following are a problem.
sequent { <H> >- LetFunDecl{| <J> >- LetFunDef {| <K> >- 'prop |} |} }
We *could* make such typings as the follows:
LetFunDecl {| Exp : TyExp >- 'a |} : 'a
But I don't know if this is so wise to let the body be so polymorphic.