Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-19 11:54:40 -0700 (Sat, 19 Apr 2003)
Revision: 4462
Log message:

      - Implemented resource annotations on rewrites (including conditional rewrites).
      - Implemented reduce resource annotations.
      - The annotations on ML rewrites are not supported (yet?), but at least they
      will now produce an error message, instead of being silently ignored.
      

Changes  Path
+10 -10 metaprl/filter/boot/rewrite_boot.ml
+3 -4 metaprl/filter/boot/tactic_boot_sig.mlz
+99 -88 metaprl/filter/filter/filter_prog.ml
+13 -11 metaprl/refiner/refiner/refine.ml
+8 -0 metaprl/refiner/reflib/mp_resource.ml
+8 -0 metaprl/refiner/reflib/mp_resource.mli
+5 -4 metaprl/refiner/refsig/refine_sig.ml
+15 -33 metaprl/theories/itt/itt_bool.ml
+11 -21 metaprl/theories/itt/itt_int_base.ml
+1 -1 metaprl/theories/itt/itt_int_base.prla
+12 -19 metaprl/theories/itt/itt_sort.ml
+2 -2 metaprl/theories/tactic/summary.ml
+2 -6 metaprl/theories/tactic/top_conversionals.ml
+5 -3 metaprl/theories/tactic/top_conversionals.mli