Commit log for MetaPRL

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-08-02 10:12:26 -0700 (Sun, 02 Aug 1998)
Revision: 2380
Log message:

      Modified rewriter to handle Alexey's new sequents.  The rewriter is
      now moved to a new directory refiner/rewrite.  Clause numbers in
      TermMan now start with 1.  The tactics seem to work, but there may
      be some lurking problems with hypothesis numbering.

Changes	Path
+11 -25	metaprl/editor/ml/test.ml
+0 -7	metaprl/editor/ml/test.mli
+36 -21	metaprl/editor/ml/x.ml
+1 -1	metaprl/filter/filter_prog.ml
+84 -3	metaprl/mllib/array_util.ml
+18 -5	metaprl/mllib/array_util.mli
+5 -0	metaprl/mllib/list_util.ml
+1 -0	metaprl/mllib/list_util.mli
+1 -0	metaprl/refiner/Makefile
+0 -1	metaprl/refiner/refiner/Files
+1 -1	metaprl/refiner/refiner/Makefile
+4 -0	metaprl/refiner/refiner/refine_error.ml
+2 -0	metaprl/refiner/refiner/refine_error.mli
Deleted	metaprl/refiner/refiner/rewrite.mlip
Deleted	metaprl/refiner/refiner/rewrite.mlp
+29 -0	metaprl/refiner/reflib/refine_exn.ml
+4 -0	metaprl/refiner/refsig/refine_error_sig.ml
+2 -0	metaprl/refiner/refsig/refiner_sig.ml
+5 -0	metaprl/refiner/refsig/term_addr_sig.ml
+6 -0	metaprl/refiner/refsig/term_base_sig.ml
+12 -1	metaprl/refiner/refsig/term_man_sig.ml
+11 -11	metaprl/refiner/refsig/term_simple_sig.mlz
+1 -0	metaprl/refiner/refsig/term_subst_sig.ml
Properties	metaprl/refiner/rewrite
Added	metaprl/refiner/rewrite/Files
Properties	metaprl/refiner/rewrite/Files
Added	metaprl/refiner/rewrite/Makefile
Properties	metaprl/refiner/rewrite/Makefile
Added	metaprl/refiner/rewrite/rewrite.mlip
Properties	metaprl/refiner/rewrite/rewrite.mlip
Added	metaprl/refiner/rewrite/rewrite.mlp
Properties	metaprl/refiner/rewrite/rewrite.mlp
Added	metaprl/refiner/rewrite/rewrite_build_contractum.mlip
Properties	metaprl/refiner/rewrite/rewrite_build_contractum.mlip
Added	metaprl/refiner/rewrite/rewrite_build_contractum.mlp
Properties	metaprl/refiner/rewrite/rewrite_build_contractum.mlp
Added	metaprl/refiner/rewrite/rewrite_build_contractum_sig.mlz
Properties	metaprl/refiner/rewrite/rewrite_build_contractum_sig.mlz
Added	metaprl/refiner/rewrite/rewrite_compile_contractum.mlip
Properties	metaprl/refiner/rewrite/rewrite_compile_contractum.mlip
Added	metaprl/refiner/rewrite/rewrite_compile_contractum.mlp
Properties	metaprl/refiner/rewrite/rewrite_compile_contractum.mlp
Added	metaprl/refiner/rewrite/rewrite_compile_contractum_sig.mlz
Properties	metaprl/refiner/rewrite/rewrite_compile_contractum_sig.mlz
Added	metaprl/refiner/rewrite/rewrite_compile_redex.mlip
Properties	metaprl/refiner/rewrite/rewrite_compile_redex.mlip
Added	metaprl/refiner/rewrite/rewrite_compile_redex.mlp
Properties	metaprl/refiner/rewrite/rewrite_compile_redex.mlp
Added	metaprl/refiner/rewrite/rewrite_compile_redex_sig.mlz
Properties	metaprl/refiner/rewrite/rewrite_compile_redex_sig.mlz
Added	metaprl/refiner/rewrite/rewrite_debug.mlip
Properties	metaprl/refiner/rewrite/rewrite_debug.mlip
Added	metaprl/refiner/rewrite/rewrite_debug.mlp
Properties	metaprl/refiner/rewrite/rewrite_debug.mlp
Added	metaprl/refiner/rewrite/rewrite_debug_sig.ml
Properties	metaprl/refiner/rewrite/rewrite_debug_sig.ml
Added	metaprl/refiner/rewrite/rewrite_match_redex.mlip
Properties	metaprl/refiner/rewrite/rewrite_match_redex.mlip
Added	metaprl/refiner/rewrite/rewrite_match_redex.mlp
Properties	metaprl/refiner/rewrite/rewrite_match_redex.mlp
Added	metaprl/refiner/rewrite/rewrite_match_redex_sig.mlz
Properties	metaprl/refiner/rewrite/rewrite_match_redex_sig.mlz
Added	metaprl/refiner/rewrite/rewrite_meta.mlip
Properties	metaprl/refiner/rewrite/rewrite_meta.mlip
Added	metaprl/refiner/rewrite/rewrite_meta.mlp
Properties	metaprl/refiner/rewrite/rewrite_meta.mlp
Added	metaprl/refiner/rewrite/rewrite_meta_sig.mlz
Properties	metaprl/refiner/rewrite/rewrite_meta_sig.mlz
Added	metaprl/refiner/rewrite/rewrite_type.mlip
Properties	metaprl/refiner/rewrite/rewrite_type.mlip
Added	metaprl/refiner/rewrite/rewrite_type.mlp
Properties	metaprl/refiner/rewrite/rewrite_type.mlp
Added	metaprl/refiner/rewrite/rewrite_type_sig.mlz
Properties	metaprl/refiner/rewrite/rewrite_type_sig.mlz
Added	metaprl/refiner/rewrite/rewrite_util.mlip
Properties	metaprl/refiner/rewrite/rewrite_util.mlip
Added	metaprl/refiner/rewrite/rewrite_util.mlp
Properties	metaprl/refiner/rewrite/rewrite_util.mlp
Added	metaprl/refiner/rewrite/rewrite_util_sig.ml
Properties	metaprl/refiner/rewrite/rewrite_util_sig.ml
+16 -7	metaprl/refiner/term_ds/term_addr_ds.mlp
+28 -27	metaprl/refiner/term_ds/term_base_ds.mlp
+44 -45	metaprl/refiner/term_ds/term_man_ds.mlp
+18 -7	metaprl/refiner/term_ds/term_subst_ds.mlp
+10 -5	metaprl/refiner/term_gen/term_addr_gen.mlp
+18 -21	metaprl/refiner/term_gen/term_man_gen.mlp
+6 -1	metaprl/refiner/term_std/term_base_std.mlp
+22 -0	metaprl/refiner/term_std/term_subst_std.mlp
+1 -1	metaprl/theories/base/base_rewrite.ml
+4 -4	metaprl/theories/czf/czf_itt_all.ml
+4 -4	metaprl/theories/czf/czf_itt_and.ml
+3 -3	metaprl/theories/czf/czf_itt_dall.ml
+3 -3	metaprl/theories/czf/czf_itt_dexists.ml
+1 -1	metaprl/theories/czf/czf_itt_empty.ml
+15 -15	metaprl/theories/czf/czf_itt_eq.ml
+5 -5	metaprl/theories/czf/czf_itt_eq_inner.ml
+4 -4	metaprl/theories/czf/czf_itt_exists.ml
+4 -4	metaprl/theories/czf/czf_itt_false.ml
+6 -6	metaprl/theories/czf/czf_itt_implies.ml
+5 -5	metaprl/theories/czf/czf_itt_member.ml
+4 -4	metaprl/theories/czf/czf_itt_or.ml
+5 -5	metaprl/theories/czf/czf_itt_pre_set.ml
+1 -1	metaprl/theories/czf/czf_itt_rel.ml
+2 -2	metaprl/theories/czf/czf_itt_sall.ml
+3 -3	metaprl/theories/czf/czf_itt_sep.ml
+5 -5	metaprl/theories/czf/czf_itt_set.ml
+6 -6	metaprl/theories/czf/czf_itt_set_ext.ml
+4 -4	metaprl/theories/czf/czf_itt_set_ind.ml
+2 -2	metaprl/theories/czf/czf_itt_sexists.ml
+11 -11	metaprl/theories/czf/czf_itt_small.ml
+4 -4	metaprl/theories/czf/czf_itt_true.ml
+2 -2	metaprl/theories/czf/czf_itt_union.ml
+4 -5	metaprl/theories/itt/itt_atom.ml
+9 -10	metaprl/theories/itt/itt_bool.ml
+1 -1	metaprl/theories/itt/itt_derive.ml
+10 -14	metaprl/theories/itt/itt_dfun.ml
+5 -5	metaprl/theories/itt/itt_dprod.ml
+18 -14	metaprl/theories/itt/itt_equal.ml
+4 -0	metaprl/theories/itt/itt_equal.mli
+6 -6	metaprl/theories/itt/itt_fun.ml
+6 -9	metaprl/theories/itt/itt_int.ml
+5 -8	metaprl/theories/itt/itt_isect.ml
+10 -13	metaprl/theories/itt/itt_list.ml
+122 -34	metaprl/theories/itt/itt_logic.ml
+10 -0	metaprl/theories/itt/itt_logic.mli
Binary	metaprl/theories/itt/itt_logic.prlb
+8 -4	metaprl/theories/itt/itt_prod.ml
+4 -0	metaprl/theories/itt/itt_prod.mli
+5 -5	metaprl/theories/itt/itt_quotient.ml
+14 -23	metaprl/theories/itt/itt_rfun.ml
+11 -15	metaprl/theories/itt/itt_set.ml
+4 -4	metaprl/theories/itt/itt_struct.ml
+2 -2	metaprl/theories/itt/itt_subtype.ml
+7 -7	metaprl/theories/itt/itt_union.ml
+9 -13	metaprl/theories/itt/itt_unit.ml
+4 -5	metaprl/theories/itt/itt_void.ml
+5 -5	metaprl/theories/itt/itt_w.ml
+2 -2	metaprl/theories/tactic/rewrite_type.ml
+19 -2	metaprl/theories/tactic/sequent.ml
+3 -1	metaprl/theories/tactic/sequent.mli
+2 -2	metaprl/theories/tactic/tactic_type.ml
+1 -1	metaprl/theories/tactic/tactic_type.mli
+3 -3	metaprl/theories/tactic/tacticals.ml
+28 -5	metaprl/theories/tptp/tptp.ml
+4 -0	metaprl/theories/tptp/tptp.mli
Binary	metaprl/theories/tptp/tptp.prlb
+43 -43	metaprl/theories/tptp/tptp_prove.ml