Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-04-04 16:35:20 -0700 (Sun, 04 Apr 1999)
Revision: 2630
Log message:

      Added the primitive support for resource improvement through
      rule annotations.  There is still no connection with the parser.
      

Changes  Path
+10 -9 metaprl/filter/filter_parse.ml
+8 -5 metaprl/filter/filter_prog.ml
+18 -12 metaprl/filter/filter_summary.ml
+6 -5 metaprl/filter/filter_summary.mli
+15 -4 metaprl/refiner/reflib/mp_resource.ml
+18 -10 metaprl/refiner/reflib/mp_resource.mli
+7 -7 metaprl/refiner/term_gen/term_meta_gen.ml
+15 -7 metaprl/theories/base/base_auto_tactic.ml
+3 -2 metaprl/theories/base/base_auto_tactic.mli
+2 -1 metaprl/theories/base/base_cache.ml
+1 -1 metaprl/theories/base/base_cache.mli
+2 -1 metaprl/theories/base/base_dtactic.ml
+1 -1 metaprl/theories/base/base_dtactic.mli
+4 -2 metaprl/theories/base/typeinf.ml
+2 -2 metaprl/theories/base/typeinf.mli
+2 -1 metaprl/theories/itt/itt_equal.ml
+2 -1 metaprl/theories/itt/itt_equal.mli
+2 -1 metaprl/theories/itt/itt_squash.ml
+1 -1 metaprl/theories/itt/itt_squash.mli
+2 -1 metaprl/theories/itt/itt_subtype.ml
+1 -1 metaprl/theories/itt/itt_subtype.mli
+10 -2 metaprl/theories/tactic/conversionals.ml
+1 -1 metaprl/theories/tactic/conversionals.mli
+2 -1 metaprl/theories/tactic/mptop.ml
+1 -1 metaprl/theories/tactic/mptop.mli
+5 -0 metaprl/util/macro.ml