Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-06-22 12:46:48 -0700 (Mon, 22 Jun 1998)
Revision: 2268
Log message:

      Rewriting in contexts.  This required a change in addressing,
      and the body of the context is the _last_ subterm, not the first.
      

Changes	Path
+1 -1	metaprl/Makefile
Properties	metaprl/editor/ml
Added	metaprl/editor/ml/y.ml
Properties	metaprl/editor/ml/y.ml
Properties	metaprl/filter
+25 -5	metaprl/filter/filter_bin.ml
+28 -6	metaprl/filter/filter_cache_fun.ml
+6 -0	metaprl/filter/filter_parse.ml
+5 -1	metaprl/filter/filter_summary_io.ml
Properties	metaprl/library
Properties	metaprl/mllib
+20 -0	metaprl/mllib/array_util.ml
+6 -0	metaprl/mllib/array_util.mli
+14 -6	metaprl/mllib/debug.ml
+7 -1	metaprl/mllib/debug.mli
+27 -0	metaprl/mllib/list_util.ml
+8 -1	metaprl/mllib/list_util.mli
Properties	metaprl/refiner
+5 -2	metaprl/refiner/Makefile
Properties	metaprl/refiner/refbase
+21 -0	metaprl/refiner/refbase/opname.ml
+5 -0	metaprl/refiner/refbase/opname.mli
Properties	metaprl/refiner/refiner
+19 -0	metaprl/refiner/refiner/refine.ml
+313 -32	metaprl/refiner/refiner/rewrite.ml
Properties	metaprl/refiner/reflib
+8 -0	metaprl/refiner/reflib/simple_print.ml
Properties	metaprl/refiner/refsig
+4 -1	metaprl/refiner/refsig/refine_sig.ml
+11 -1	metaprl/refiner/refsig/term_addr_sig.ml
+8 -0	metaprl/refiner/refsig/term_simple_sig.mlz
Properties	metaprl/refiner/term_ds
+45 -14	metaprl/refiner/term_ds/term_ds.ml
+5 -0	metaprl/refiner/term_ds/term_ds.mli
+80 -23	metaprl/refiner/term_ds/term_subst_ds.ml
Properties	metaprl/refiner/term_gen
+61 -40	metaprl/refiner/term_gen/term_addr_gen.ml
+47 -16	metaprl/refiner/term_gen/term_man_gen.ml
Properties	metaprl/refiner/term_std
+30 -9	metaprl/refiner/term_std/term_std.ml
+9 -0	metaprl/refiner/term_std/term_std.mli
+28 -15	metaprl/refiner/term_std/term_subst_std.ml
Properties	metaprl/theories/base
+23 -0	metaprl/theories/base/base_dform.ml
+9 -6	metaprl/theories/base/base_rewrite.ml
+10 -4	metaprl/theories/base/base_rewrite.mli
Properties	metaprl/theories/czf
+10 -5	metaprl/theories/czf/czf_itt_or.ml
+5 -1	metaprl/theories/czf/czf_itt_or.mli
+29 -5	metaprl/theories/czf/czf_itt_wf.ml
+15 -3	metaprl/theories/czf/czf_itt_wf.mli
+0 -3	metaprl/theories/itt/Makefile
+6 -2	metaprl/theories/itt/itt_atom.ml
+11 -7	metaprl/theories/itt/itt_dprod.ml
+6 -2	metaprl/theories/itt/itt_dprod.mli
+18 -2	metaprl/theories/itt/itt_equal.ml
+16 -0	metaprl/theories/itt/itt_equal.mli
+6 -1	metaprl/theories/itt/itt_list.ml
+8 -0	metaprl/theories/itt/itt_list.mli
+8 -0	metaprl/theories/itt/itt_logic.ml
+7 -2	metaprl/theories/itt/itt_quotient.ml
+8 -0	metaprl/theories/itt/itt_quotient.mli
+5 -0	metaprl/theories/itt/itt_rfun.ml
+5 -1	metaprl/theories/itt/itt_struct.ml
+7 -1	metaprl/theories/itt/itt_subtype.ml
+8 -0	metaprl/theories/itt/itt_subtype.mli
Deleted	metaprl/theories/itt/itt_theory.mlz
+7 -3	metaprl/theories/itt/itt_union.ml
+6 -2	metaprl/theories/itt/itt_union.mli
Properties	metaprl/theories/ocaml
+1 -2	metaprl/theories/ocaml/Makefile
Deleted	metaprl/theories/ocaml/perv.ml
Deleted	metaprl/theories/ocaml/perv.mli
Properties	metaprl/theories/ocaml_sos
Properties	metaprl/theories/rewrite
Properties	metaprl/theories/tactic
+4 -3	metaprl/theories/tactic/Makefile
+17 -0	metaprl/theories/tactic/conversionals.ml
+6 -0	metaprl/theories/tactic/conversionals.mli
Added	metaprl/theories/tactic/perv.ml
Properties	metaprl/theories/tactic/perv.ml
Added	metaprl/theories/tactic/perv.mli
Properties	metaprl/theories/tactic/perv.mli
+163 -18	metaprl/theories/tactic/rewrite_type.ml
+44 -0	metaprl/theories/tactic/rewrite_type.mli
+21 -2	metaprl/theories/tactic/tactic_type.ml
+6 -0	metaprl/theories/tactic/tacticals.ml
+5 -0	metaprl/theories/tactic/tacticals.mli