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