Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-27 17:59:01 -0700 (Sun, 27 Jun 2004)
Revision: 6030
Log message:

      Refiner.Refiner.RefineError is now included in Basic_tactics
      

Changes	Path
+2 -1	metaprl/OMakefile
+0 -1	metaprl/editor/ml/shell_p4.ml
+1 -0	metaprl/filter/filter/filter_prog.ml
+2 -3	metaprl/refiner/refiner/refine.ml
+2 -3	metaprl/refiner/refiner/refine.mli
+6 -8	metaprl/refiner/refiner/refine_error.ml
+6 -12	metaprl/refiner/refiner/refine_error.mli
+1 -1	metaprl/refiner/refsig/Files
+9 -15	metaprl/refiner/refsig/refine_error_sig.ml
+2 -8	metaprl/refiner/refsig/refiner_sig.ml
+1 -8	metaprl/refiner/rewrite/rewrite.ml
+1 -7	metaprl/refiner/rewrite/rewrite.mli
+1 -7	metaprl/refiner/rewrite/rewrite_build_contractum.ml
+1 -7	metaprl/refiner/rewrite/rewrite_build_contractum.mli
+1 -5	metaprl/refiner/rewrite/rewrite_compile_contractum.ml
+1 -5	metaprl/refiner/rewrite/rewrite_compile_contractum.mli
+1 -5	metaprl/refiner/rewrite/rewrite_compile_redex.ml
+1 -5	metaprl/refiner/rewrite/rewrite_compile_redex.mli
+1 -5	metaprl/refiner/rewrite/rewrite_debug.ml
+1 -5	metaprl/refiner/rewrite/rewrite_debug.mli
+1 -7	metaprl/refiner/rewrite/rewrite_match_redex.ml
+1 -7	metaprl/refiner/rewrite/rewrite_match_redex.mli
+1 -5	metaprl/refiner/rewrite/rewrite_meta.ml
+1 -5	metaprl/refiner/rewrite/rewrite_meta.mli
+1 -5	metaprl/refiner/rewrite/rewrite_util.ml
+1 -5	metaprl/refiner/rewrite/rewrite_util.mli
+2 -2	metaprl/refiner/term_ds/term_addr_ds.ml
+2 -2	metaprl/refiner/term_ds/term_addr_ds.mli
+4 -4	metaprl/refiner/term_ds/term_base_ds.ml
+4 -4	metaprl/refiner/term_ds/term_base_ds.mli
+4 -4	metaprl/refiner/term_ds/term_eval_ds.ml
+4 -4	metaprl/refiner/term_ds/term_eval_ds.mli
+2 -2	metaprl/refiner/term_ds/term_man_ds.ml
+2 -2	metaprl/refiner/term_ds/term_man_ds.mli
+4 -4	metaprl/refiner/term_ds/term_op_ds.ml
+4 -4	metaprl/refiner/term_ds/term_op_ds.mli
+4 -4	metaprl/refiner/term_ds/term_subst_ds.ml
+4 -4	metaprl/refiner/term_ds/term_subst_ds.mli
+2 -2	metaprl/refiner/term_gen/term_addr_gen.ml
+2 -2	metaprl/refiner/term_gen/term_addr_gen.mli
+1 -2	metaprl/refiner/term_gen/term_man_gen.ml
+1 -1	metaprl/refiner/term_gen/term_man_gen.mli
+1 -3	metaprl/refiner/term_gen/term_meta_gen.ml
+1 -3	metaprl/refiner/term_gen/term_meta_gen.mli
+1 -6	metaprl/refiner/term_std/term_base_std.ml
+1 -5	metaprl/refiner/term_std/term_base_std.mli
+1 -5	metaprl/refiner/term_std/term_eval_std.ml
+1 -5	metaprl/refiner/term_std/term_eval_std.mli
+1 -6	metaprl/refiner/term_std/term_op_std.ml
+1 -5	metaprl/refiner/term_std/term_op_std.mli
+1 -6	metaprl/refiner/term_std/term_subst_std.ml
+1 -5	metaprl/refiner/term_std/term_subst_std.mli
+1 -0	metaprl/support/shell/browser_resource.ml
+1 -0	metaprl/support/tactics/basic_tactics.ml
+1 -0	metaprl/support/tactics/simp_typeinf.ml
+1 -0	metaprl/support/tactics/top_conversionals.ml
+0 -1	metaprl/theories/czf/czf_itt_equiv.ml
+1 -1	metaprl/theories/experimental/compile/m_cps.mli
+0 -1	metaprl/theories/experimental/compile/m_x86_spill.ml
+0 -1	metaprl/theories/itt/itt_fset.ml
+0 -1	metaprl/theories/itt/itt_fun.ml
+0 -1	metaprl/theories/itt/itt_int_base.ml
+0 -1	metaprl/theories/itt/itt_isect.ml
+0 -1	metaprl/theories/itt/itt_logic.ml
+0 -1	metaprl/theories/itt/itt_mpoly2.ml
+0 -1	metaprl/theories/itt/itt_mpoly3.ml
+0 -1	metaprl/theories/itt/itt_quotient.ml
+0 -1	metaprl/theories/itt/itt_rat.ml
+0 -1	metaprl/theories/itt/itt_record_label.ml
+0 -1	metaprl/theories/itt/itt_squash.ml
+0 -1	metaprl/theories/itt/itt_struct2.ml
+0 -1	metaprl/theories/itt/itt_subtype.ml
+0 -1	metaprl/theories/itt/itt_supinf.ml
+0 -1	metaprl/theories/mesa/ma_decidable__equality.ml
+0 -1	metaprl/theories/sil/sil_itt_sos.ml
+0 -1	metaprl/theories/tptp/tptp.ml
+0 -1	metaprl/theories/tptp/tptp_prove.ml
+2 -2	metaprl/util/ocamldep.mll