Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-02-25 16:37:49 -0800 (Thu, 25 Feb 1999)
Revision: 2602
Log message:

      Made TermHeader, TermHash and TermNorm a part of the term module
      

Changes	Path
+8 -0	metaprl/refiner/refiner/refiner_ds.ml
+8 -0	metaprl/refiner/refiner/refiner_std.ml
+0 -4	metaprl/refiner/reflib/Files
+27 -48	metaprl/refiner/reflib/term_copy2_weak.ml
+2 -34	metaprl/refiner/reflib/term_copy2_weak.mli
+4 -19	metaprl/refiner/reflib/term_copy_weak.ml
+4 -20	metaprl/refiner/reflib/term_copy_weak.mli
Deleted	metaprl/refiner/reflib/term_hash.ml
Deleted	metaprl/refiner/reflib/term_hash.mli
Deleted	metaprl/refiner/reflib/term_header.ml
Deleted	metaprl/refiner/reflib/term_header.mli
Deleted	metaprl/refiner/reflib/term_header_constr.ml
Deleted	metaprl/refiner/reflib/term_header_constr.mli
+1 -7	metaprl/refiner/reflib/term_io.ml
Deleted	metaprl/refiner/reflib/term_norm.ml
Deleted	metaprl/refiner/reflib/term_norm.mli
+3 -2	metaprl/refiner/refsig/Files
+27 -1	metaprl/refiner/refsig/refiner_sig.ml
Added	metaprl/refiner/refsig/term_norm_sig.ml
Properties	metaprl/refiner/refsig/term_norm_sig.ml
+29 -4	metaprl/refiner/refsig/termmod_hash_sig.ml
+5 -1	metaprl/refiner/term_gen/Files
Added	metaprl/refiner/term_gen/term_hash.ml
Properties	metaprl/refiner/term_gen/term_hash.ml
Added	metaprl/refiner/term_gen/term_hash.mli
Properties	metaprl/refiner/term_gen/term_hash.mli
Added	metaprl/refiner/term_gen/term_header.ml
Properties	metaprl/refiner/term_gen/term_header.ml
Added	metaprl/refiner/term_gen/term_header.mli
Properties	metaprl/refiner/term_gen/term_header.mli
Added	metaprl/refiner/term_gen/term_header_constr.ml
Properties	metaprl/refiner/term_gen/term_header_constr.ml
Added	metaprl/refiner/term_gen/term_header_constr.mli
Properties	metaprl/refiner/term_gen/term_header_constr.mli
Added	metaprl/refiner/term_gen/term_norm.ml
Properties	metaprl/refiner/term_gen/term_norm.ml
Added	metaprl/refiner/term_gen/term_norm.mli
Properties	metaprl/refiner/term_gen/term_norm.mli