Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-04-21 12:55:23 -0700 (Tue, 21 Apr 1998)
Revision: 2145
Log message:

      Upgraded refiner for program extraction.
      

Changes	Path
+5 -2	metaprl/filter/filter_cache_fun.ml
+5 -2	metaprl/filter/filter_parse.ml
+87 -53	metaprl/filter/filter_prog.ml
+9 -6	metaprl/filter/filter_prog.mli
+39 -14	metaprl/filter/filter_summary.ml
+4 -1	metaprl/filter/filter_summary.mli
+4 -1	metaprl/mllib/array_util.ml
+4 -1	metaprl/mllib/array_util.mli
+95 -57	metaprl/mllib/list_util.ml
+22 -14	metaprl/mllib/list_util.mli
+938 -360	metaprl/refiner/refine.ml
+5 -0	metaprl/refiner/refine_exn.ml
+145 -73	metaprl/refiner/refine_sig.ml
+23 -16	metaprl/refiner/rewrite.ml
+4 -1	metaprl/refiner/rformat.ml
+26 -26	metaprl/refiner/term.ml
+5 -1	metaprl/refiner/term.mli
+4 -1	metaprl/theories/base/typeinf.ml
Properties	metaprl/theories/itt
+6 -1	metaprl/theories/itt/itt_equal.ml
+7 -3	metaprl/theories/itt/itt_squash.ml
+4 -1	metaprl/theories/itt/itt_subtype.ml
+12 -8	metaprl/theories/tactic/sequent.ml
+4 -1	metaprl/theories/tactic/tactic_type.mlz
+117 -78	metaprl/theories/tactic/tacticals.ml