Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-09 05:23:47 -0800 (Tue, 09 Mar 2004)
Revision: 5443
Log message:

      Removing the distinction between the Hypothesis and HypBinding - it was
      causing too much trouble unnecessarily complicating a lot of code.
      
      The IO part of the distinction is still there - on IO the "unused" bindings
      are interpreted as variables with an empty "string" part.
      

Changes  Path
+6 -3 metaprl/filter/base/filter_magic.ml
+1 -2 metaprl/filter/base/filter_type.ml
+2 -5 metaprl/filter/filter/filter_parse.ml
+1 -4 metaprl/filter/filter/filter_patt.ml
+9 -9 metaprl/filter/filter/term_grammar.ml
+18 -66 metaprl/refiner/refiner/refine.ml
+10 -10 metaprl/refiner/reflib/ascii_io.ml
+5 -5 metaprl/refiner/reflib/dform.ml
+3 -6 metaprl/refiner/reflib/match_seq.ml
+5 -7 metaprl/refiner/reflib/refine_exn.ml
+9 -17 metaprl/refiner/reflib/simple_print.ml
+1 -2 metaprl/refiner/reflib/term_compare.ml
+1 -3 metaprl/refiner/reflib/term_match_table.ml
+0 -1 metaprl/refiner/refsig/refine_sig.ml
+3 -4 metaprl/refiner/refsig/term_hash_sig.ml
+0 -1 metaprl/refiner/refsig/term_man_minimal_sig.ml
+0 -2 metaprl/refiner/refsig/term_man_sig.ml
+3 -3 metaprl/refiner/refsig/term_meta_sig.ml
+4 -5 metaprl/refiner/refsig/term_sig.ml
+1 -2 metaprl/refiner/rewrite/rewrite.ml
+5 -15 metaprl/refiner/rewrite/rewrite_build_contractum.ml
+2 -9 metaprl/refiner/rewrite/rewrite_compile_contractum.ml
+5 -13 metaprl/refiner/rewrite/rewrite_compile_redex.ml
+2 -5 metaprl/refiner/rewrite/rewrite_debug.ml
+7 -18 metaprl/refiner/rewrite/rewrite_match_redex.ml
+1 -2 metaprl/refiner/rewrite/rewrite_types.ml
+8 -11 metaprl/refiner/term_ds/term_addr_ds.ml
+4 -10 metaprl/refiner/term_ds/term_base_ds.ml
+15 -38 metaprl/refiner/term_ds/term_man_ds.ml
+4 -8 metaprl/refiner/term_ds/term_op_ds.ml
+4 -9 metaprl/refiner/term_ds/term_subst_ds.ml
+7 -16 metaprl/refiner/term_gen/term_hash.ml
+1 -2 metaprl/refiner/term_gen/term_header_constr.ml
+6 -42 metaprl/refiner/term_gen/term_man_gen.ml
+40 -23 metaprl/refiner/term_gen/term_meta_gen.ml
+23 -32 metaprl/support/display/base_dform.ml
+1 -1 metaprl/support/tactics/auto_tactic.ml
+84 -89 metaprl/support/tactics/dtactic.ml
+1 -9 metaprl/support/tactics/tactic_cache.ml
+3 -7 metaprl/support/tactics/top_tacticals.ml
+1 -8 metaprl/support/tactics/typeinf.ml
+1 -3 metaprl/tactics/proof/proof_boot.ml
+1 -1 metaprl/tactics/proof/sequent_boot.ml
+1 -1 metaprl/tactics/proof/tactic_boot.ml
+1 -1 metaprl/theories/itt/itt_int_arith.ml
+34 -45 metaprl/theories/itt/itt_logic.ml
+2 -2 metaprl/theories/itt/itt_squash.ml
+3 -3 metaprl/theories/tptp/tptp_load.ml
+4 -4 metaprl/theories/tptp/tptp_prove.ml
+1 -2 mpcompiler/mmc/core/mmc_core_closure.ml
+2 -1 mpcompiler/mmc/core/mmc_core_type_check.ml
+9 -12 mpcompiler/mmc/core/mmc_core_type_infer.ml