Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-26 10:53:54 -0700 (Thu, 26 Jun 2003)
Revision: 4688
Log message:

      Deleting some code that was added during a recent attempt to make the extraction work.
      That code (allowing more than one mention of the same seq. condext among redexes)
      was incomplete, not quite valid and not the right way to go anyway.
      

Changes  Path
+1 -1 metaprl/refiner/rewrite/rewrite_build_contractum.ml
+1 -6 metaprl/refiner/rewrite/rewrite_compile_redex.ml
+0 -3 metaprl/refiner/rewrite/rewrite_debug.ml
+0 -41 metaprl/refiner/rewrite/rewrite_match_redex.ml
+0 -1 metaprl/refiner/rewrite/rewrite_types.ml