Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-11-15 15:03:47 -0800 (Thu, 15 Nov 2001)
Revision: 3444
Log message:

      Code cleanup:
      
      I looked (using the code I've put into macro.ml) for places where the same code
      appeared in several branches of a match or function expression. I changed those
      places to use a complex pattern and a single copy of the code.
      

Changes  Path
+3 -5 metaprl/editor/ml/proof_edit.ml
+8 -10 metaprl/editor/ml/shell.ml
+3 -4 metaprl/editor/ml/shell_mp.ml
+3 -6 metaprl/editor/ml/shell_package.ml
+28 -45 metaprl/filter/base/filter_comment.ml
+19 -35 metaprl/filter/base/filter_summary.ml
+29 -51 metaprl/filter/base/free_vars.ml
+84 -139 metaprl/filter/base/mLast_util.ml
+2 -4 metaprl/filter/base/term_grammar.ml
+34 -71 metaprl/filter/boot/proof_boot.ml
+7 -12 metaprl/filter/boot/proof_term_boot.ml
+3 -5 metaprl/filter/filter/filter_parse.ml
+2 -7 metaprl/mllib/comment_parse.mll
+5 -6 metaprl/mllib/file_util.ml
+10 -12 metaprl/mllib/flist.ml
+1 -3 metaprl/mllib/http_server.ml
+19 -56 metaprl/mllib/red_black_set.ml
+26 -70 metaprl/mllib/red_black_table.ml
+22 -34 metaprl/mllib/splay_linear_set.ml
+3 -5 metaprl/mllib/splay_table.ml
+57 -116 metaprl/refiner/refiner/refine.ml
+5 -12 metaprl/refiner/rewrite/rewrite.ml
+1 -2 metaprl/refiner/rewrite/rewrite_build_contractum.ml
+18 -14 metaprl/refiner/rewrite/rewrite_meta.ml
+13 -19 metaprl/refiner/rewrite/rewrite_util.ml
+1 -2 metaprl/refiner/term_ds/term_addr_ds.ml
+1 -2 metaprl/refiner/term_ds/term_unif_ds.ml
+9 -18 metaprl/refiner/term_gen/term_meta_gen.ml
+4 -8 metaprl/refiner/term_gen/term_shape_gen.ml
+4 -6 metaprl/theories/base/base_meta.ml
+1 -2 metaprl/theories/itt/itt_logic.ml
+2 -3 metaprl/theories/itt/itt_squash.ml
+7 -16 metaprl/theories/tactic/mptop.ml
+1 -2 metaprl/theories/tactic/tactic_cache.ml
+18 -2 metaprl/util/macro.ml