Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-04 18:15:05 -0800 (Tue, 04 Nov 2003)
Revision: 5071
Log message:

      Changing the order of arguments in apply_subst to make it easier to use
      it in functions like List.map.
      

Changes  Path
+2 -2 metaprl/refiner/reflib/unify_mm.ml
+1 -1 metaprl/refiner/refsig/term_subst_sig.ml
+7 -9 metaprl/refiner/term_ds/term_subst_ds.ml
+2 -2 metaprl/refiner/term_std/term_subst_std.ml
+1 -1 metaprl/support/tactics/simp_typeinf.ml
+1 -1 metaprl/support/tactics/typeinf.ml
+2 -2 metaprl/theories/itt/itt_equal.ml
+11 -11 metaprl/theories/itt/itt_logic.ml
+3 -3 mpcompiler/mmc/core/mmc_core_type_infer.ml

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2003-11-12 14:28:53 -0800 (Wed, 12 Nov 2003)
Revision: 5092
Log message:

      Automatically prove the 2'nd subgoal of type inference.
      

Changes  Path
+4 -2 mpcompiler/mmc/core/mmc_core_type_infer.ml

Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2003-11-12 17:30:39 -0800 (Wed, 12 Nov 2003)
Revision: 5094
Log message:

      Added type checking rule for Return, added type checking to CPS rule.
      

Changes  Path
+4 -1 mpcompiler/mmc/core/mmc_core_cps.ml
+12 -2 mpcompiler/mmc/core/mmc_core_type_check.ml