Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-02-25 09:59:51 -0800 (Thu, 25 Feb 1999)
Revision: 2601
Log message:

      1) Functorized the Term_copy[2]_weak/Term_hash/Termm_header/etc modules
      correctly, now it should be easy make the Term_hash module
      a part of the refiner
      
      2) Created a new Term_io module that provides Refiner_std <-> Refiner
      convertion based on the term_copy2_weak, these functions are now used
      instead of the old Term_copy functions
      
      3) Removed old Term_copy - related modules
      

Changes  Path
+2 -4 metaprl/editor/ml/package_info.ml
+8 -12 metaprl/editor/ml/proof.ml
+9 -13 metaprl/filter/filter_cache.ml
+4 -4 metaprl/mllib/Makefile
Deleted metaprl/mllib/bi_memo.ml
Deleted metaprl/mllib/bi_memo.mli
+1 -0 metaprl/mllib/weak_memo.ml
+6 -47 metaprl/mllib/weak_memo.mli
Added metaprl/mllib/weak_memo_sig.ml
Properties metaprl/mllib/weak_memo_sig.ml
+2 -2 metaprl/refiner/refbase/Makefile
+2 -2 metaprl/refiner/refiner/Makefile
+7 -9 metaprl/refiner/reflib/Files
+2 -2 metaprl/refiner/reflib/Makefile
+5 -5 metaprl/refiner/reflib/ml_term.ml
Deleted metaprl/refiner/reflib/term_copy.ml
Deleted metaprl/refiner/reflib/term_copy.mli
Deleted metaprl/refiner/reflib/term_copy2.ml
Deleted metaprl/refiner/reflib/term_copy2.mli
+46 -23 metaprl/refiner/reflib/term_copy2_weak.ml
+36 -20 metaprl/refiner/reflib/term_copy2_weak.mli
+22 -15 metaprl/refiner/reflib/term_copy_weak.ml
+20 -19 metaprl/refiner/reflib/term_copy_weak.mli
+61 -113 metaprl/refiner/reflib/term_hash.ml
+19 -66 metaprl/refiner/reflib/term_hash.mli
+6 -0 metaprl/refiner/reflib/term_header.ml
+9 -147 metaprl/refiner/reflib/term_header.mli
+49 -35 metaprl/refiner/reflib/term_header_constr.ml
+23 -9 metaprl/refiner/reflib/term_header_constr.mli
Added metaprl/refiner/reflib/term_io.ml
Properties metaprl/refiner/reflib/term_io.ml
Added metaprl/refiner/reflib/term_io.mli
Properties metaprl/refiner/reflib/term_io.mli
+20 -4 metaprl/refiner/reflib/term_norm.ml
+31 -16 metaprl/refiner/reflib/term_norm.mli
Deleted metaprl/refiner/reflib/term_transfer.ml
Deleted metaprl/refiner/reflib/term_transfer.mli
+4 -1 metaprl/refiner/refsig/Files
+2 -2 metaprl/refiner/refsig/Makefile
Added metaprl/refiner/refsig/term_hash_sig.ml
Properties metaprl/refiner/refsig/term_hash_sig.ml
Added metaprl/refiner/refsig/term_header_sig.mlz
Properties metaprl/refiner/refsig/term_header_sig.mlz
Added metaprl/refiner/refsig/termmod_hash_sig.ml
Properties metaprl/refiner/refsig/termmod_hash_sig.ml
+2 -2 metaprl/refiner/rewrite/Makefile
+2 -2 metaprl/refiner/term_ds/Makefile
+2 -2 metaprl/refiner/term_gen/Makefile
+2 -2 metaprl/refiner/term_std/Makefile