Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-02 15:25:40 -0700 (Thu, 02 Jul 1998)
Revision: 2284
Log message:

      Created term_copy module to copy and normalize terms.
      

Changes	Path
+5 -2	metaprl/filter/filter_bin.ml
+74 -12	metaprl/filter/filter_cache.ml
+9 -6	metaprl/filter/filter_cache_fun.ml
+4 -1	metaprl/filter/filter_parse.ml
+14 -11	metaprl/filter/filter_prog.ml
+15 -12	metaprl/filter/filter_prog.mli
+161 -173	metaprl/filter/filter_summary.ml
+128 -107	metaprl/filter/filter_summary.mli
+10 -7	metaprl/filter/filter_summary_type.mlz
+9 -6	metaprl/filter/filter_summary_util.mli
Added	metaprl/mllib/memo.ml
Properties	metaprl/mllib/memo.ml
Added	metaprl/mllib/memo.mli
Properties	metaprl/mllib/memo.mli
+4 -1	metaprl/refiner/refiner/refiner.ml
+1 -0	metaprl/refiner/reflib/Files
+12 -10	metaprl/refiner/reflib/ml_term.ml
Added	metaprl/refiner/reflib/term_copy.ml
Properties	metaprl/refiner/reflib/term_copy.ml
Added	metaprl/refiner/reflib/term_copy.mli
Properties	metaprl/refiner/reflib/term_copy.mli
+3 -6	metaprl/refiner/refsig/term_base_sig.ml
+3 -1	metaprl/refiner/refsig/term_meta_sig.ml
+4 -1	metaprl/refiner/refsig/term_simple_sig.mlz
+26 -44	metaprl/refiner/term_ds/term_base_ds.mlp
+1 -1	metaprl/refiner/term_ds/term_ds.ml
+4 -2	metaprl/refiner/term_ds/term_ds_sig.ml
+9 -9	metaprl/refiner/term_ds/term_eval_ds.mlp
+77 -77	metaprl/refiner/term_ds/term_op_ds.mlp
+14 -14	metaprl/refiner/term_ds/term_subst_ds.mlp
+24 -21	metaprl/refiner/term_gen/term_man_gen.mlp
+3 -15	metaprl/refiner/term_gen/term_meta_gen.mlp
+2 -2	metaprl/refiner/term_gen/term_shape_gen.mlp
+33 -42	metaprl/refiner/term_std/term_base_std.mlp
+12 -9	metaprl/refiner/term_std/term_eval_std.mlp
+77 -74	metaprl/refiner/term_std/term_op_std.mlp
+4 -1	metaprl/refiner/term_std/term_std.ml
+4 -2	metaprl/refiner/term_std/term_std_sig.ml
+23 -20	metaprl/refiner/term_std/term_subst_std.mlp
Deleted	metaprl/theories/ocaml/ocaml_df.ml
Deleted	metaprl/theories/ocaml/ocaml_df.mli
+12 -0	metaprl/theories/ocaml/ocaml_expr_df.ml
+0 -1	metaprl/theories/tactic/Makefile
+7 -4	metaprl/theories/tactic/conversionals.ml
+5 -3	metaprl/theories/tactic/conversionals.mli
Deleted	metaprl/theories/tactic/options.ml
Deleted	metaprl/theories/tactic/options.mli
+65 -12	metaprl/theories/tactic/rewrite_type.ml
+5 -1	metaprl/theories/tactic/rewrite_type.mli
+39 -2	metaprl/theories/tactic/sequent.ml
+37 -3	metaprl/theories/tactic/sequent.mli
+10 -6	metaprl/theories/tactic/tactic_cache.ml
+86 -64	metaprl/theories/tactic/tactic_type.ml
+14 -22	metaprl/theories/tactic/tactic_type.mli
+18 -10	metaprl/theories/tactic/tacticals.ml
+11 -7	metaprl/theories/tactic/tacticals.mli
+13 -0	metaprl/theories/tactic/var.ml
+8 -4	metaprl/theories/tactic/var.mli