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.
      

Changes  Path
+24 -36 metaprl-branches/opname_classes2/filter/base/filter_cache_fun.ml
+4 -4 metaprl-branches/opname_classes2/filter/filter/filter_parse.ml
+11 -4 metaprl-branches/opname_classes2/filter/filter/term_grammar.ml
+2 -6 metaprl-branches/opname_classes2/refiner/reflib/refine_exn.ml
+118 -18 metaprl-branches/opname_classes2/refiner/reflib/term_ty_infer.ml
+7 -0 metaprl-branches/opname_classes2/refiner/reflib/term_ty_infer.mli
+60 -5 metaprl-branches/opname_classes2/support/display/perv.ml
+4 -3 metaprl-branches/opname_classes2/support/display/perv.mli
+23 -19 metaprl-branches/opname_classes2/theories/base/base_meta.ml
+20 -19 metaprl-branches/opname_classes2/theories/base/base_meta.mli
+1 -1 mpcompiler-branches/opname_classes2/mmc/base/mmc_base_hoist.ml
+1 -1 mpcompiler-branches/opname_classes2/mmc/base/mmc_base_hoist.mli
+1 -1 mpcompiler-branches/opname_classes2/mmc/base/mmc_base_meta.ml
+1 -1 mpcompiler-branches/opname_classes2/mmc/base/mmc_base_meta.mli
+48 -30 mpcompiler-branches/opname_classes2/mmc/core/mmc_core_ast.ml
+53 -29 mpcompiler-branches/opname_classes2/mmc/core/mmc_core_ast.mli
+1 -1 mpcompiler-branches/opname_classes2/mmc/core/mmc_core_closure.ml
+1 -1 mpcompiler-branches/opname_classes2/mmc/core/mmc_core_closure.mli
+4 -4 mpcompiler-branches/opname_classes2/mmc/core/mmc_core_cps.mli
+1 -1 mpcompiler-branches/opname_classes2/mmc/core/mmc_core_front.mli
+3 -3 mpcompiler-branches/opname_classes2/mmc/core/mmc_core_inline.mli
+2 -1 mpcompiler-branches/opname_classes2/mmc/core/mmc_core_list_util.mli
+2 -2 mpcompiler-branches/opname_classes2/mmc/core/mmc_core_reserve.mli
+15 -4 mpcompiler-branches/opname_classes2/mmc/core/mmc_core_tast.ml
+40 -13 mpcompiler-branches/opname_classes2/mmc/core/mmc_core_tast.mli
+50 -45 mpcompiler-branches/opname_classes2/mmc/core/mmc_core_type_check.ml
+4 -7 mpcompiler-branches/opname_classes2/mmc/core/mmc_core_type_check.mli
+4 -4 mpcompiler-branches/opname_classes2/mmc/core/mmc_core_type_util.mli
+5 -4 mpcompiler-branches/opname_classes2/mmc/core/mmc_core_value.mli
+9 -8 mpcompiler-branches/opname_classes2/util/mm_arith_util.ml
+8 -7 mpcompiler-branches/opname_classes2/util/mm_arith_util.mli
+6 -5 mpcompiler-branches/opname_classes2/util/mm_dform_util.ml
+4 -4 mpcompiler-branches/opname_classes2/util/mm_dform_util.mli
+16 -9 mpcompiler-branches/opname_classes2/util/mm_list_util.ml
+10 -6 mpcompiler-branches/opname_classes2/util/mm_list_util.mli