Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-14 16:25:26 -0800 (Fri, 14 Nov 2003)
Revision: 5100
Log message:

      - This is a new approach to handling internal GC in weak_memo - instead
      of relying on OCaml runtime to do the right thing, just count the GC generations
      and include it in the weak descriptors. Note that this change should make the
      3.06 vs 3.07+2 distinction irrelevant.
      
      - This also eliminates the retrieve vs retrieve_hack distinction - now retrieve
      just takes the anchor off the descriptor and it does not require passing the
      whole info as an argument.
      
      Yegor, please take a look when you have time. Thanks!
      

Changes  Path
+47 -86 metaprl-branches/ocaml_3_07/mllib/weak_memo.ml
+1 -8 metaprl-branches/ocaml_3_07/mllib/weak_memo_sig.ml
+12 -36 metaprl-branches/ocaml_3_07/refiner/reflib/term_copy2_weak.ml
+19 -27 metaprl-branches/ocaml_3_07/refiner/reflib/term_copy2_weak.mli
+3 -6 metaprl-branches/ocaml_3_07/refiner/reflib/term_copy_weak.ml
+6 -6 metaprl-branches/ocaml_3_07/refiner/refsig/term_hash_sig.ml
+6 -6 metaprl-branches/ocaml_3_07/refiner/refsig/term_norm_sig.ml
+4 -4 metaprl-branches/ocaml_3_07/refiner/term_ds/term_base_ds.ml
+1 -1 metaprl-branches/ocaml_3_07/refiner/term_ds/term_subst_ds.ml
+17 -24 metaprl-branches/ocaml_3_07/refiner/term_gen/term_hash.ml
+3 -6 metaprl-branches/ocaml_3_07/refiner/term_gen/term_norm.ml
+1 -1 metaprl-branches/ocaml_3_07/refiner/term_std/term_base_std.ml
+46 -77 metaprl-branches/ocaml_3_07/tactics/proof/proof_term_boot.ml