Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-21 15:55:44 -0800 (Sun, 21 Mar 2004)
Revision: 5509
Log message:

      - Changed the dtactic module to use the new API
      (note: this changes the selT semantics slightly and adds full fall-back
      to both intro and elim).
      - Changed the compilers to use the new API.
      - Changed the get_bool_arg, get_sel_arg and get_int_arg to return an option
      instead of raising exception (since we always catch those exceptions anyway).
      
      MetaPRL finally compiles with the new API (but does not really run yet).
      

Changes  Path
+6 -3 metaprl-branches/new_match_table/filter/base/filter_magic.ml
+5 -0 metaprl-branches/new_match_table/filter/base/filter_summary.ml
+12 -12 metaprl-branches/new_match_table/support/tactics/auto_tactic.ml
+27 -119 metaprl-branches/new_match_table/support/tactics/dtactic.ml
+2 -3 metaprl-branches/new_match_table/support/tactics/simp_typeinf.ml
+2 -3 metaprl-branches/new_match_table/support/tactics/top_conversionals.ml
+4 -5 metaprl-branches/new_match_table/support/tactics/typeinf.ml
+10 -10 metaprl-branches/new_match_table/tactics/proof/tactic_boot.ml
+7 -7 metaprl-branches/new_match_table/tactics/proof/tactic_boot_sig.ml
+2 -6 metaprl-branches/new_match_table/tactics/proof/tacticals_boot.ml
+1 -1 metaprl-branches/new_match_table/theories/experimental/compile/m_closure.ml
+1 -1 metaprl-branches/new_match_table/theories/experimental/compile/m_cps.ml
+1 -1 metaprl-branches/new_match_table/theories/experimental/compile/m_dead.ml
+1 -1 metaprl-branches/new_match_table/theories/experimental/compile/m_ir_ast.ml
+1 -1 metaprl-branches/new_match_table/theories/experimental/compile/m_prog.ml
+1 -2 metaprl-branches/new_match_table/theories/experimental/compile/m_util.ml
+0 -1 metaprl-branches/new_match_table/theories/experimental/compile/m_util.mli
+2 -2 metaprl-branches/new_match_table/theories/experimental/compile/m_x86_opt.ml
+1 -1 metaprl-branches/new_match_table/theories/experimental/compile/m_x86_spill.ml
+14 -33 metaprl-branches/new_match_table/theories/itt/itt_bisect.ml
+5 -7 metaprl-branches/new_match_table/theories/itt/itt_disect.ml
+15 -33 metaprl-branches/new_match_table/theories/itt/itt_esquash.ml
+11 -31 metaprl-branches/new_match_table/theories/itt/itt_fun.ml
+4 -4 metaprl-branches/new_match_table/theories/itt/itt_int_base.ml
+3 -2 metaprl-branches/new_match_table/theories/itt/itt_logic.ml
+1 -3 metaprl-branches/new_match_table/theories/itt/itt_quotient.ml
+4 -4 metaprl-branches/new_match_table/theories/itt/itt_record.ml
+1 -1 mpcompiler-branches/new_match_table/mmc/core/mmc_core_cps.ml
+1 -1 mpcompiler-branches/new_match_table/mmc/core/mmc_core_name.ml
+1 -1 mpcompiler-branches/new_match_table/mmc/core/mmc_core_type_erase.ml
+1 -1 mpcompiler-branches/new_match_table/mmc/core/mmc_core_type_util.ml
+1 -2 mpcompiler-branches/new_match_table/mmc/core/mmc_core_util.ml
+0 -1 mpcompiler-branches/new_match_table/mmc/core/mmc_core_util.mli