Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-24 17:29:42 -0700 (Thu, 24 Apr 2003)
Revision: 4485
Log message:

      Got rid of the HTML "tagges zone" code (which was used anyway).
      

Changes	Path
+0 -1	metaprl/doc/latex/theories/Makefile
+1 -1	metaprl/filter/base/filter_cache_fun.ml
+4 -4	metaprl/filter/boot/tactic_boot_sig.mlz
+1 -5	metaprl/refiner/reflib/dform.ml
+1 -1	metaprl/refiner/reflib/dform.mli
+31 -108	metaprl/refiner/reflib/rformat.ml
+30 -31	metaprl/refiner/reflib/rformat.mli
+1 -1	metaprl/refiner/reflib/simple_print.ml
+1 -1	metaprl/refiner/reflib/simple_print_sig.ml