Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2004-01-21 16:29:08 -0800 (Wed, 21 Jan 2004)
Revision: 5268
Log message:

      Changed the meta_term and hypothesis type definitions in term_sig
      to avoid type duplication.
      
      The new type definitions are toplevel as polymorphic types.  For example
      
      |   type 'term poly_hypothesis = Hypothesis of 'term | ...
      
      Then, once the term type is defined, we can use the following
      definition:
      
      |   type hypothesis = term poly_hypothesis
      
      This is in preparation for extending the hypothesis type with
      cases for recursive sequents.
      

Changes  Path
+1 -0 metaprl/filter/base/filter_summary.ml
+1 -0 metaprl/filter/base/filter_util.ml
+1 -0 metaprl/filter/filter/filter_parse.ml
+4 -4 metaprl/filter/filter/filter_patt.ml
+1 -0 metaprl/filter/filter/term_grammar.ml
+3 -2 metaprl/refiner/reflib/arith.ml
+3 -3 metaprl/refiner/reflib/ascii_io.ml
+1 -0 metaprl/refiner/reflib/dform.ml
+2 -1 metaprl/refiner/reflib/match_seq.ml
+1 -0 metaprl/refiner/reflib/ml_format.ml
+1 -0 metaprl/refiner/reflib/refine_exn.ml
+1 -1 metaprl/refiner/reflib/simple_print.ml
+3 -3 metaprl/refiner/reflib/term_compare.ml
+1 -0 metaprl/refiner/reflib/term_match_table.ml
+12 -10 metaprl/refiner/refsig/term_sig.ml
+1 -0 metaprl/refiner/term_ds/term_addr_ds.ml
+1 -0 metaprl/refiner/term_ds/term_base_ds.ml
+3 -14 metaprl/refiner/term_ds/term_ds.ml
+3 -10 metaprl/refiner/term_ds/term_ds_sig.ml
+2 -2 metaprl/refiner/term_ds/term_man_ds.ml
+1 -0 metaprl/refiner/term_ds/term_op_ds.ml
+1 -0 metaprl/refiner/term_ds/term_subst_ds.ml
+8 -8 metaprl/refiner/term_gen/term_hash.ml
+8 -8 metaprl/refiner/term_gen/term_header_constr.ml
+3 -14 metaprl/refiner/term_std/term_std.ml
+3 -10 metaprl/refiner/term_std/term_std_sig.ml
+1 -0 metaprl/support/display/base_dform.ml
+1 -0 metaprl/support/shell/shell_rule.ml
+1 -0 metaprl/support/tactics/dtactic.ml
+3 -3 metaprl/support/tactics/tactic_cache.ml
+1 -0 metaprl/support/tactics/top_tacticals.ml
+1 -0 metaprl/support/tactics/typeinf.ml
+2 -1 metaprl/theories/experimental/compile/m_util.ml
+3 -12 metaprl/theories/itt/itt_int_arith.ml
+1 -0 metaprl/theories/itt/itt_logic.ml
+13 -39 metaprl/theories/itt/itt_squash.ml
+20 -5 metaprl/theories/itt/itt_supinf.ml
+1 -0 metaprl/theories/tptp/tptp_load.ml
+1 -0 metaprl/theories/tptp/tptp_prove.ml
+14 -14 mpcompiler/mmc/core/mmc_core_closure.ml
+5 -4 mpcompiler/mmc/core/mmc_core_type_infer.ml
+1 -0 mpcompiler/mmc/core/mmc_core_util.ml