Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-19 21:38:32 -0700 (Thu, 19 May 2005)
Revision: 7305
Log message:

      Use Lm_symbol.eq instead of (=) more consistently.
      

Changes  Path
+1 -1 metaprl/refiner/refiner/refiner_debug.ml
+1 -1 metaprl/refiner/reflib/match_seq.ml
+7 -7 metaprl/refiner/reflib/term_compare.ml
+1 -1 metaprl/refiner/reflib/unify_mm.ml
+2 -2 metaprl/refiner/rewrite/rewrite_match_redex.ml
+1 -1 metaprl/refiner/rewrite/rewrite_util.ml
+2 -2 metaprl/refiner/term_ds/term_addr_ds.ml
+1 -1 metaprl/refiner/term_ds/term_base_ds.ml
+4 -4 metaprl/refiner/term_ds/term_man_ds.ml
+18 -18 metaprl/refiner/term_ds/term_subst_ds.ml
+1 -1 metaprl/refiner/term_gen/term_addr_gen.ml
+6 -6 metaprl/refiner/term_gen/term_hash.ml
+4 -4 metaprl/refiner/term_gen/term_man_gen.ml
+2 -2 metaprl/refiner/term_std/term_subst_std.ml
+1 -1 metaprl/support/tactics/dtactic.ml
+1 -1 metaprl/support/tactics/top_tacticals.ml
+1 -1 metaprl/theories/itt/itt_logic.ml