Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-06-30 21:38:04 -0700 (Tue, 30 Jun 1998)
Revision: 2280
Log message:

      Moved Refiner exceptions into a separate module RefineErrors
      

Changes	Path
+4 -0	metaprl/editor/ml/proof.ml
+4 -1	metaprl/editor/ml/proof.mli
+4 -0	metaprl/editor/ml/proof_edit.ml
+5 -1	metaprl/editor/ml/proof_step.ml
+4 -1	metaprl/editor/ml/shell.ml
+4 -1	metaprl/editor/ml/shell_null.ml
+4 -0	metaprl/editor/ml/shell_rewrite.ml
+4 -0	metaprl/editor/ml/shell_rule.ml
+1 -0	metaprl/refiner/refiner/Files
+17 -38	metaprl/refiner/refiner/refine.ml
+9 -2	metaprl/refiner/refiner/refine.mli
Added	metaprl/refiner/refiner/refine_errors.ml
Properties	metaprl/refiner/refiner/refine_errors.ml
Added	metaprl/refiner/refiner/refine_errors.mli
Properties	metaprl/refiner/refiner/refine_errors.mli
+6 -2	metaprl/refiner/refiner/refiner_ds.ml
+6 -2	metaprl/refiner/refiner/refiner_std.ml
+85 -105	metaprl/refiner/refiner/rewrite.ml
+12 -3	metaprl/refiner/refiner/rewrite.mli
+6 -3	metaprl/refiner/reflib/refine_exn.ml
+4 -2	metaprl/refiner/reflib/refine_exn.mli
Properties	metaprl/refiner/refsig
+1 -0	metaprl/refiner/refsig/Files
Added	metaprl/refiner/refsig/refine_errors_sig.mlz
Properties	metaprl/refiner/refsig/refine_errors_sig.mlz
+3 -30	metaprl/refiner/refsig/refine_sig.ml
+10 -3	metaprl/refiner/refsig/refiner_sig.ml
+3 -22	metaprl/refiner/refsig/rewrite_sig.ml
+4 -1	metaprl/theories/base/base_dtactic.ml
+4 -1	metaprl/theories/base/base_rewrite.ml
+4 -1	metaprl/theories/base/typeinf.ml
+4 -1	metaprl/theories/czf/czf_itt_all.ml
+4 -1	metaprl/theories/czf/czf_itt_and.ml
+4 -1	metaprl/theories/czf/czf_itt_dall.ml
+4 -1	metaprl/theories/czf/czf_itt_dexists.ml
+4 -1	metaprl/theories/czf/czf_itt_exists.ml
+4 -1	metaprl/theories/czf/czf_itt_false.ml
+4 -1	metaprl/theories/czf/czf_itt_implies.ml
+4 -1	metaprl/theories/czf/czf_itt_or.ml
+4 -1	metaprl/theories/czf/czf_itt_set.ml
+4 -1	metaprl/theories/czf/czf_itt_true.ml
+4 -1	metaprl/theories/czf/czf_itt_wf.ml
+4 -1	metaprl/theories/itt/itt_arith.ml
+4 -1	metaprl/theories/itt/itt_dfun.ml
+4 -1	metaprl/theories/itt/itt_dprod.ml
+7 -4	metaprl/theories/itt/itt_equal.ml
+4 -1	metaprl/theories/itt/itt_fun.ml
+4 -1	metaprl/theories/itt/itt_int.ml
+4 -1	metaprl/theories/itt/itt_isect.ml
+6 -2	metaprl/theories/itt/itt_list.ml
+4 -1	metaprl/theories/itt/itt_logic.ml
+4 -1	metaprl/theories/itt/itt_prod.ml
+4 -1	metaprl/theories/itt/itt_quotient.ml
+4 -1	metaprl/theories/itt/itt_rfun.ml
+4 -1	metaprl/theories/itt/itt_set.ml
+4 -1	metaprl/theories/itt/itt_squash.ml
+4 -1	metaprl/theories/itt/itt_struct.ml
+4 -1	metaprl/theories/itt/itt_subtype.ml
+5 -2	metaprl/theories/itt/itt_union.ml
+4 -1	metaprl/theories/tactic/conversionals.ml
+4 -1	metaprl/theories/tactic/conversionals.mli
+5 -1	metaprl/theories/tactic/rewrite_type.ml
+4 -0	metaprl/theories/tactic/tactic_cache.ml
+4 -0	metaprl/theories/tactic/tactic_type.ml
+4 -1	metaprl/theories/tactic/tacticals.ml