Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-12-08 10:12:55 -0800 (Mon, 08 Dec 2003)
Revision: 5169
Log message:

      Clean up some weird code (which is currently unused anyway since it concerns
      ML rules).
      

Changes  Path
+1 -1 metaprl/filter/filter/filter_prog.ml
+9 -18 metaprl/tactics/proof/tactic_boot.ml
+1 -1 metaprl/tactics/proof/tactic_boot_sig.ml