Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-06-09 13:53:04 -0700 (Tue, 09 Jun 1998)
Revision: 2222
Log message:

      Propagated refinement changes.
      New tacticals module.
      

Changes	Path
Properties	metaprl/editor/ml
+2 -0	metaprl/editor/ml/Makefile
+72 -40	metaprl/editor/ml/io_proof.ml
+7 -3	metaprl/editor/ml/io_proof_type.mlz
+8 -2	metaprl/editor/ml/package_info.ml
+8 -1	metaprl/editor/ml/package_info.mli
+6 -0	metaprl/editor/ml/package_type.mlz
+12 -13	metaprl/editor/ml/proof.ml
+6 -0	metaprl/editor/ml/proof.mli
+11 -14	metaprl/editor/ml/proof_step.ml
+6 -0	metaprl/editor/ml/proof_step.mli
Added	metaprl/editor/ml/proof_type.mlz
Properties	metaprl/editor/ml/proof_type.mlz
+11 -3	metaprl/editor/ml/shell_rewrite.ml
Added	metaprl/editor/ml/x.ml
Properties	metaprl/editor/ml/x.ml
+9 -5	metaprl/filter/filter_prog.ml
+10 -89	metaprl/refiner/Makefile
+0 -1	metaprl/refiner/reflib/Files
+10 -5	metaprl/refiner/reflib/term_dtable.ml
+70 -154	metaprl/refiner/reflib/term_stable.ml
+14 -11	metaprl/refiner/reflib/term_stable.mli
Deleted	metaprl/refiner/reflib/term_template.ml
Deleted	metaprl/refiner/reflib/term_template.mli
+4 -3	metaprl/refiner/refsig/refine_sig.ml
+16 -1	metaprl/refiner/refsig/term_man_sig.ml
+84 -37	metaprl/refiner/term_gen/term_man_gen.ml
+5 -1	metaprl/theories/base/base_dtactic.ml
+5 -1	metaprl/theories/base/typeinf.ml
+26 -21	metaprl/theories/itt/itt_dfun.ml
+9 -6	metaprl/theories/itt/itt_dprod.ml
+5 -1	metaprl/theories/itt/itt_equal.ml
+7 -4	metaprl/theories/itt/itt_fun.ml
+7 -4	metaprl/theories/itt/itt_int.ml
+8 -5	metaprl/theories/itt/itt_isect.ml
+7 -4	metaprl/theories/itt/itt_list.ml
+7 -4	metaprl/theories/itt/itt_prod.ml
+8 -4	metaprl/theories/itt/itt_quotient.ml
+10 -7	metaprl/theories/itt/itt_rfun.ml
+30 -28	metaprl/theories/itt/itt_set.ml
+5 -1	metaprl/theories/itt/itt_squash.ml
+22 -21	metaprl/theories/itt/itt_struct.ml
+7 -4	metaprl/theories/itt/itt_subtype.ml
+16 -8	metaprl/theories/itt/itt_union.ml
+6 -2	metaprl/theories/itt/itt_unit.ml
+6 -3	metaprl/theories/itt/itt_void.ml
+26 -21	metaprl/theories/tactic/options.ml
+9 -7	metaprl/theories/tactic/options.mli
+37 -46	metaprl/theories/tactic/sequent.ml
+27 -13	metaprl/theories/tactic/sequent.mli
+581 -431	metaprl/theories/tactic/tactic_cache.ml
+13 -7	metaprl/theories/tactic/tactic_cache.mli
+700 -51	metaprl/theories/tactic/tactic_type.ml
+95 -31	metaprl/theories/tactic/tactic_type.mli
+88 -179	metaprl/theories/tactic/tacticals.ml
+28 -16	metaprl/theories/tactic/tacticals.mli