Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-11-06 11:21:55 -0800 (Thu, 06 Nov 2003)
Revision: 5075
Log message:

      In this branch I switching WeakMemo from incremental GCion to "full" GCion. Instead of multiplying mutexes/conditional variables I use lists of mutually recursive tables and weakmemo-users are responsible for keeping them correct.
      

Changes  Path
+14 -0 metaprl/mllib/hash_with_gc.ml
+1 -0 metaprl/mllib/hash_with_gc_sig.ml
+1 -1 metaprl/mllib/memo.ml
+1 -0 metaprl/mllib/memo_sig.ml
+140 -42 metaprl/mllib/weak_memo.ml
+9 -0 metaprl/mllib/weak_memo_sig.ml
+22 -9 metaprl/refiner/reflib/term_copy2_weak.ml
+1 -1 metaprl/refiner/reflib/term_copy2_weak.mli
+3 -1 metaprl/refiner/refsig/term_hash_sig.ml
+23 -7 metaprl/refiner/term_gen/term_hash.ml
+12 -12 metaprl/tactics/proof/proof_term_boot.ml