Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-23 11:40:34 -0700 (Thu, 23 Jul 1998)
Revision: 2347
Log message:

      Moved eseqent type to the TermType module.
      Made the types of esequent components hidden to make them read-only.
      

Changes  Path
+2 -2 metaprl/filter/term_grammar.ml
+1 -0 metaprl/refiner/refsig/refiner_sig.ml
+1 -8 metaprl/refiner/refsig/term_man_sig.ml
+24 -0 metaprl/refiner/refsig/term_simple_sig.mlz
+30 -0 metaprl/refiner/term_ds/term_ds.ml
+11 -0 metaprl/refiner/term_ds/term_ds_sig.ml
+1 -0 metaprl/refiner/term_gen/term_man_gen.mlip
+7 -14 metaprl/refiner/term_gen/term_man_gen.mlp
+30 -0 metaprl/refiner/term_std/term_std.ml
+11 -0 metaprl/refiner/term_std/term_std_sig.ml
+3 -2 metaprl/theories/base/base_auto_tactic.ml
+9 -8 metaprl/theories/base/base_dform.ml
+3 -2 metaprl/theories/base/typeinf.ml
+5 -4 metaprl/theories/itt/itt_arith.ml
+4 -3 metaprl/theories/itt/itt_logic.ml
+5 -4 metaprl/theories/tactic/tactic_cache.ml