Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-08-25 22:54:44 -0700 (Wed, 25 Aug 2004)
Revision: 6141
Log message:
The MMC part of the df_context commit I just made. With this change, I
get the correct behavior for contexts in LetFun* sequents:
# << LetFunDecl{| <H>; f: 'ty >- LetFunDef{| <J> ; FunDef{'f; 'def[]} >- 'f |} |} >>;;
(* Recursive functions: <?\239?\191?\189?\239?\191?\189>, f : !ty *) let rec <?\239?\191?\189?\239?\191?\189> and f = def in f : term