Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-05 20:31:39 -0700 (Fri, 05 May 2000)
Revision: 2957
Log message:

      I replaced Cycle and Clash exceptions in unify_ds with
      RefineError's and tried to run tests/tptp-gen.ml
      
      For some reason it never terminates.
      

Changes	Path
+1 -3	metaprl-branches/unify_mm/editor/ml/shell.ml
+23 -26	metaprl-branches/unify_mm/refiner/term_ds/term_unif_ds.ml
+1 -1	metaprl-branches/unify_mm/theories/tptp/tptp_prove.ml