Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-30 19:25:44 -0800 (Sun, 30 Jan 2005)
Revision: 6531
Log message:

      Whew, the rules in mmc_core_type_check.ml now type check.
      Added hypothesis and universal types.  So we now have:
      
      declare sequent { all a : TyProp. TyElem{'a} : 'a >- ('b :> TyProp) } : Judgment
      

Changes  Path
+15 -7 metaprl-branches/opname_classes2/filter/filter/term_grammar.ml
+367 -138 metaprl-branches/opname_classes2/refiner/reflib/term_ty_infer.ml
+5 -3 metaprl-branches/opname_classes2/refiner/reflib/term_ty_infer.mli
+1 -0 metaprl-branches/opname_classes2/refiner/refsig/term_meta_sig.ml
+14 -0 metaprl-branches/opname_classes2/refiner/term_gen/term_meta_gen.ml
+23 -31 metaprl-branches/opname_classes2/support/display/perv.ml
+8 -5 metaprl-branches/opname_classes2/support/display/perv.mli
+1 -1 mpcompiler-branches/opname_classes2/mmc/base/mmc_base_judgment.ml
+1 -1 mpcompiler-branches/opname_classes2/mmc/base/mmc_base_judgment.mli
+1 -1 mpcompiler-branches/opname_classes2/mmc/core/mmc_core_type_check.ml