Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-03-09 09:19:13 -0800 (Wed, 09 Mar 2005)
Revision: 6869
Log message:

      Convert "std" lambdas to "rec" lambdas during type inference.
      I'm not sure exactly the difference between "rec" and "std",
      but let's work with it for now.
      
      Also, I renamed Sequent.explode_sequent to Sequent.explode_sequent_arg
      to avoid the shadowing hassle with TermMan.explode_sequent.
      

Changes  Path
+1 -3 metaprl/refiner/term_ds/term_op_ds.ml
+1 -3 metaprl/refiner/term_std/term_op_std.ml
+0 -0 metaprl/support/tactics/OMakefile
+1 -1 metaprl/support/tactics/top_tacticals.ml
+2 -2 metaprl/tactics/proof/sequent_boot.ml
+1 -1 metaprl/tactics/proof/tactic_boot_sig.ml
+4 -4 metaprl/tactics/proof/tacticals_boot.ml
+1 -1 metaprl/theories/itt/itt_int_arith.ml
+2 -2 metaprl/theories/itt/itt_logic.ml
+2 -2 metaprl/theories/itt/itt_omega.ml
+1 -1 metaprl/theories/itt/itt_squash.ml
+1 -1 metaprl/theories/itt/itt_supinf.ml
+3 -10 metaprl/theories/tptp/tptp_prove.ml
+9 -0 mpcompiler/mmc/core/mmc_core_ast.ml
+0 -0 mpcompiler/mmc/core/mmc_core_cps.ml
+5 -1 mpcompiler/mmc/core/mmc_core_tast.ml
+7 -0 mpcompiler/mmc/core/mmc_core_tast.mli
+10 -6 mpcompiler/mmc/core/mmc_core_type_check.ml
+1 -1 mpcompiler/mmc/core/mmc_core_type_erase.ml
+90 -93 mpcompiler/mmc/core/mmc_core_type_infer.ml