Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-02 11:38:08 -0700 (Thu, 02 Jul 1998)
Revision: 2283
Log message:

      Refiner modules now raise RefineError exceptions directly.
      Modules in this revision have two versions: one that raises
      verbose exceptions, and another that uses a generic exception.
      

Changes  Path
+17 -12 metaprl/editor/emacs/nuprl.el
+1 -1 metaprl/editor/ml/Makefile
+32 -26 metaprl/editor/ml/io_proof.ml
+6 -0 metaprl/editor/ml/package_df.ml
+74 -53 metaprl/editor/ml/package_info.ml
+6 -2 metaprl/editor/ml/package_info.mli
+6 -1 metaprl/editor/ml/package_type.mlz
+59 -19 metaprl/editor/ml/proof.ml
+13 -5 metaprl/editor/ml/proof.mli
+46 -11 metaprl/editor/ml/proof_edit.ml
+7 -1 metaprl/editor/ml/proof_edit.mli
+51 -17 metaprl/editor/ml/proof_step.ml
+11 -3 metaprl/editor/ml/proof_step.mli
+7 -2 metaprl/editor/ml/proof_type.mlz
+8 -16 metaprl/editor/ml/shell.ml
+7 -9 metaprl/editor/ml/shell.mli
+6 -1 metaprl/editor/ml/shell_null.ml
+72 -31 metaprl/editor/ml/shell_rewrite.ml
+6 -1 metaprl/editor/ml/shell_rewrite.mli
+67 -26 metaprl/editor/ml/shell_rule.ml
+6 -1 metaprl/editor/ml/shell_rule.mli
+12 -7 metaprl/editor/ml/y.ml
+13 -0 metaprl/filter/filter_cache.ml
+6 -0 metaprl/filter/filter_cache.mli
+8 -1 metaprl/filter/filter_ocaml.ml
+19 -5 metaprl/filter/filter_parse.ml
+92 -15 metaprl/filter/filter_prog.ml
+8 -1 metaprl/filter/filter_summary.ml
+6 -0 metaprl/filter/filter_util.ml
+6 -0 metaprl/filter/prlcomp.ml
+8 -1 metaprl/filter/term_grammar.ml
+1 -0 metaprl/library/basic.ml
+8 -10 metaprl/library/db.ml
+15 -14 metaprl/library/definition.ml
+9 -10 metaprl/library/library.ml
+2 -2 metaprl/library/library_eval.ml
+4 -5 metaprl/library/link.ml
+1 -8 metaprl/library/mbterm.ml
+1 -0 metaprl/library/nuprl5.ml
+13 -15 metaprl/library/orb.ml
+23 -1 metaprl/mk/config
+2 -1 metaprl/mllib/Makefile
+10 -1 metaprl/mllib/debug.ml
+2 -2 metaprl/refiner/Makefile
Properties metaprl/refiner/refiner
+7 -2 metaprl/refiner/refiner/Files
+1 -0 metaprl/refiner/refiner/Makefile
+428 -243 metaprl/refiner/refiner/refine.ml
+21 -13 metaprl/refiner/refiner/refine.mli
Added metaprl/refiner/refiner/refine_error.ml
Properties metaprl/refiner/refiner/refine_error.ml
Added metaprl/refiner/refiner/refine_error.mli
Properties metaprl/refiner/refiner/refine_error.mli
Deleted metaprl/refiner/refiner/refine_errors.ml
Deleted metaprl/refiner/refiner/refine_errors.mli
+8 -1 metaprl/refiner/refiner/refiner.ml
+20 -12 metaprl/refiner/refiner/refiner_ds.ml
+6 -1 metaprl/refiner/refiner/refiner_ds.mli
Added metaprl/refiner/refiner/refiner_ds_simp.ml
Properties metaprl/refiner/refiner/refiner_ds_simp.ml
Added metaprl/refiner/refiner/refiner_ds_simp.mli
Properties metaprl/refiner/refiner/refiner_ds_simp.mli
+18 -11 metaprl/refiner/refiner/refiner_std.ml
+6 -1 metaprl/refiner/refiner/refiner_std.mli
Added metaprl/refiner/refiner/refiner_std_simp.ml
Properties metaprl/refiner/refiner/refiner_std_simp.ml
Added metaprl/refiner/refiner/refiner_std_simp.mli
Properties metaprl/refiner/refiner/refiner_std_simp.mli
Deleted metaprl/refiner/refiner/rewrite.ml
Deleted metaprl/refiner/refiner/rewrite.mli
Added metaprl/refiner/refiner/rewrite.mlip
Properties metaprl/refiner/refiner/rewrite.mlip
Added metaprl/refiner/refiner/rewrite.mlp
Properties metaprl/refiner/refiner/rewrite.mlp
+6 -0 metaprl/refiner/reflib/dform.ml
+6 -0 metaprl/refiner/reflib/ml_format.ml
+81 -111 metaprl/refiner/reflib/refine_exn.ml
+7 -3 metaprl/refiner/reflib/refine_exn.mli
+6 -0 metaprl/refiner/reflib/simple_print.ml
+6 -1 metaprl/refiner/reflib/term_dtable.ml
Properties metaprl/refiner/refsig
+2 -1 metaprl/refiner/refsig/Files
Added metaprl/refiner/refsig/refine_error.h
Properties metaprl/refiner/refsig/refine_error.h
Added metaprl/refiner/refsig/refine_error_sig.ml
Properties metaprl/refiner/refsig/refine_error_sig.ml
Added metaprl/refiner/refsig/refine_error_sig.mli
Properties metaprl/refiner/refsig/refine_error_sig.mli
Deleted metaprl/refiner/refsig/refine_errors_sig.mlz
+30 -10 metaprl/refiner/refsig/refine_sig.ml
+44 -22 metaprl/refiner/refsig/refiner_sig.ml
+6 -1 metaprl/refiner/refsig/rewrite_sig.ml
+9 -5 metaprl/refiner/refsig/term_addr_sig.ml
Added metaprl/refiner/refsig/term_base_sig.ml
Properties metaprl/refiner/refsig/term_base_sig.ml
+6 -10 metaprl/refiner/refsig/term_meta_sig.ml
+8 -0 metaprl/refiner/refsig/term_op_sig.ml
+13 -68 metaprl/refiner/refsig/term_simple_sig.mlz
Properties metaprl/refiner/term_ds
+7 -2 metaprl/refiner/term_ds/Files
+3 -1 metaprl/refiner/term_ds/Makefile
Added metaprl/refiner/term_ds/term_base_ds.mlip
Properties metaprl/refiner/term_ds/term_base_ds.mlip
Added metaprl/refiner/term_ds/term_base_ds.mlp
Properties metaprl/refiner/term_ds/term_base_ds.mlp
+12 -341 metaprl/refiner/term_ds/term_ds.ml
+2 -146 metaprl/refiner/term_ds/term_ds.mli
Added metaprl/refiner/term_ds/term_ds_sig.ml
Properties metaprl/refiner/term_ds/term_ds_sig.ml
Deleted metaprl/refiner/term_ds/term_eval_ds.ml
Deleted metaprl/refiner/term_ds/term_eval_ds.mli
Added metaprl/refiner/term_ds/term_eval_ds.mlip
Properties metaprl/refiner/term_ds/term_eval_ds.mlip
Added metaprl/refiner/term_ds/term_eval_ds.mlp
Properties metaprl/refiner/term_ds/term_eval_ds.mlp
Deleted metaprl/refiner/term_ds/term_op_ds.ml
Deleted metaprl/refiner/term_ds/term_op_ds.mli
Added metaprl/refiner/term_ds/term_op_ds.mlip
Properties metaprl/refiner/term_ds/term_op_ds.mlip
Added metaprl/refiner/term_ds/term_op_ds.mlp
Properties metaprl/refiner/term_ds/term_op_ds.mlp
Deleted metaprl/refiner/term_ds/term_subst_ds.ml
Deleted metaprl/refiner/term_ds/term_subst_ds.mli
Added metaprl/refiner/term_ds/term_subst_ds.mlip
Properties metaprl/refiner/term_ds/term_subst_ds.mlip
Added metaprl/refiner/term_ds/term_subst_ds.mlp
Properties metaprl/refiner/term_ds/term_subst_ds.mlp
Properties metaprl/refiner/term_gen
+5 -1 metaprl/refiner/term_gen/Files
+1 -0 metaprl/refiner/term_gen/Makefile
Deleted metaprl/refiner/term_gen/term_addr_gen.ml
Deleted metaprl/refiner/term_gen/term_addr_gen.mli
Added metaprl/refiner/term_gen/term_addr_gen.mlip
Properties metaprl/refiner/term_gen/term_addr_gen.mlip
Added metaprl/refiner/term_gen/term_addr_gen.mlp
Properties metaprl/refiner/term_gen/term_addr_gen.mlp
Added metaprl/refiner/term_gen/term_exn.ml
Properties metaprl/refiner/term_gen/term_exn.ml
Added metaprl/refiner/term_gen/term_exn.mli
Properties metaprl/refiner/term_gen/term_exn.mli
Deleted metaprl/refiner/term_gen/term_man_gen.ml
Deleted metaprl/refiner/term_gen/term_man_gen.mli
Added metaprl/refiner/term_gen/term_man_gen.mlip
Properties metaprl/refiner/term_gen/term_man_gen.mlip
Added metaprl/refiner/term_gen/term_man_gen.mlp
Properties metaprl/refiner/term_gen/term_man_gen.mlp
Deleted metaprl/refiner/term_gen/term_meta_gen.ml
Deleted metaprl/refiner/term_gen/term_meta_gen.mli
Added metaprl/refiner/term_gen/term_meta_gen.mlip
Properties metaprl/refiner/term_gen/term_meta_gen.mlip
Added metaprl/refiner/term_gen/term_meta_gen.mlp
Properties metaprl/refiner/term_gen/term_meta_gen.mlp
Deleted metaprl/refiner/term_gen/term_shape_gen.ml
Deleted metaprl/refiner/term_gen/term_shape_gen.mli
Added metaprl/refiner/term_gen/term_shape_gen.mlip
Properties metaprl/refiner/term_gen/term_shape_gen.mlip
Added metaprl/refiner/term_gen/term_shape_gen.mlp
Properties metaprl/refiner/term_gen/term_shape_gen.mlp
Properties metaprl/refiner/term_std
+7 -2 metaprl/refiner/term_std/Files
+5 -1 metaprl/refiner/term_std/Makefile
Added metaprl/refiner/term_std/term_base_std.mlip
Properties metaprl/refiner/term_std/term_base_std.mlip
Added metaprl/refiner/term_std/term_base_std.mlp
Properties metaprl/refiner/term_std/term_base_std.mlp
Deleted metaprl/refiner/term_std/term_eval_std.ml
Deleted metaprl/refiner/term_std/term_eval_std.mli
Added metaprl/refiner/term_std/term_eval_std.mlip
Properties metaprl/refiner/term_std/term_eval_std.mlip
Added metaprl/refiner/term_std/term_eval_std.mlp
Properties metaprl/refiner/term_std/term_eval_std.mlp
Deleted metaprl/refiner/term_std/term_op_std.ml
Deleted metaprl/refiner/term_std/term_op_std.mli
Added metaprl/refiner/term_std/term_op_std.mlip
Properties metaprl/refiner/term_std/term_op_std.mlip
Added metaprl/refiner/term_std/term_op_std.mlp
Properties metaprl/refiner/term_std/term_op_std.mlp
+15 -231 metaprl/refiner/term_std/term_std.ml
+7 -127 metaprl/refiner/term_std/term_std.mli
Added metaprl/refiner/term_std/term_std_sig.ml
Properties metaprl/refiner/term_std/term_std_sig.ml
Deleted metaprl/refiner/term_std/term_subst_std.ml
Deleted metaprl/refiner/term_std/term_subst_std.mli
Added metaprl/refiner/term_std/term_subst_std.mlip
Properties metaprl/refiner/term_std/term_subst_std.mlip
Added metaprl/refiner/term_std/term_subst_std.mlp
Properties metaprl/refiner/term_std/term_subst_std.mlp
+7 -2 metaprl/theories/base/base_cache.ml
+7 -2 metaprl/theories/base/base_cache.mli
+8 -2 metaprl/theories/base/base_dform.ml
+9 -3 metaprl/theories/base/base_dtactic.ml
+10 -1 metaprl/theories/base/base_dtactic.mli
+7 -2 metaprl/theories/base/base_rewrite.ml
+6 -1 metaprl/theories/base/base_rewrite.mli
+1 -0 metaprl/theories/base/evaluator.ml
+39 -6 metaprl/theories/base/summary.ml
+10 -5 metaprl/theories/base/typeinf.ml
+8 -2 metaprl/theories/base/typeinf.mli
+2 -2 metaprl/theories/czf/Makefile
+8 -3 metaprl/theories/czf/czf_itt_all.ml
+8 -3 metaprl/theories/czf/czf_itt_all.mli
+7 -2 metaprl/theories/czf/czf_itt_and.ml
+8 -3 metaprl/theories/czf/czf_itt_and.mli
+13 -8 metaprl/theories/czf/czf_itt_dall.ml
+10 -5 metaprl/theories/czf/czf_itt_dall.mli
+13 -6 metaprl/theories/czf/czf_itt_dexists.ml
+10 -4 metaprl/theories/czf/czf_itt_dexists.mli
+7 -2 metaprl/theories/czf/czf_itt_exists.ml
+6 -1 metaprl/theories/czf/czf_itt_exists.mli
+9 -4 metaprl/theories/czf/czf_itt_false.ml
+7 -2 metaprl/theories/czf/czf_itt_false.mli
+14 -2 metaprl/theories/czf/czf_itt_implies.ml
+10 -1 metaprl/theories/czf/czf_itt_implies.mli
+7 -2 metaprl/theories/czf/czf_itt_or.ml
+6 -1 metaprl/theories/czf/czf_itt_or.mli
+250 -82 metaprl/theories/czf/czf_itt_set.ml
+160 -53 metaprl/theories/czf/czf_itt_set.mli
+8 -3 metaprl/theories/czf/czf_itt_true.ml
+6 -1 metaprl/theories/czf/czf_itt_true.mli
Deleted metaprl/theories/czf/czf_itt_wf.ml
Deleted metaprl/theories/czf/czf_itt_wf.mli
+1 -0 metaprl/theories/itt/Makefile
+6 -1 metaprl/theories/itt/itt_arith.ml
+6 -1 metaprl/theories/itt/itt_atom.mli
+6 -1 metaprl/theories/itt/itt_bool.mli
+7 -7 metaprl/theories/itt/itt_dfun.ml
+6 -1 metaprl/theories/itt/itt_dfun.mli
+47 -9 metaprl/theories/itt/itt_dprod.ml
+21 -2 metaprl/theories/itt/itt_dprod.mli
+99 -10 metaprl/theories/itt/itt_equal.ml
+51 -9 metaprl/theories/itt/itt_equal.mli
+10 -9 metaprl/theories/itt/itt_fun.ml
+7 -2 metaprl/theories/itt/itt_fun.mli
+7 -2 metaprl/theories/itt/itt_int.ml
+7 -2 metaprl/theories/itt/itt_int.mli
+8 -8 metaprl/theories/itt/itt_isect.ml
+7 -2 metaprl/theories/itt/itt_isect.mli
+8 -5 metaprl/theories/itt/itt_list.ml
+7 -2 metaprl/theories/itt/itt_list.mli
+11 -12 metaprl/theories/itt/itt_logic.ml
+34 -10 metaprl/theories/itt/itt_prod.ml
+15 -2 metaprl/theories/itt/itt_prod.mli
+8 -8 metaprl/theories/itt/itt_quotient.ml
+7 -2 metaprl/theories/itt/itt_quotient.mli
+9 -7 metaprl/theories/itt/itt_rfun.ml
+7 -2 metaprl/theories/itt/itt_rfun.mli
+15 -14 metaprl/theories/itt/itt_set.ml
+6 -1 metaprl/theories/itt/itt_set.mli
+24 -7 metaprl/theories/itt/itt_soft.ml
+9 -2 metaprl/theories/itt/itt_soft.mli
+10 -6 metaprl/theories/itt/itt_squash.ml
+24 -19 metaprl/theories/itt/itt_squash.mli
+12 -33 metaprl/theories/itt/itt_struct.ml
+6 -13 metaprl/theories/itt/itt_struct.mli
+11 -15 metaprl/theories/itt/itt_subtype.ml
+8 -2 metaprl/theories/itt/itt_subtype.mli
+10 -12 metaprl/theories/itt/itt_test.ml
+10 -15 metaprl/theories/itt/itt_union.ml
+7 -2 metaprl/theories/itt/itt_union.mli
+7 -2 metaprl/theories/itt/itt_unit.ml
+7 -2 metaprl/theories/itt/itt_unit.mli
+7 -2 metaprl/theories/itt/itt_void.ml
+7 -2 metaprl/theories/itt/itt_void.mli
Added metaprl/theories/itt/itt_w.ml
Properties metaprl/theories/itt/itt_w.ml
Added metaprl/theories/itt/itt_w.mli
Properties metaprl/theories/itt/itt_w.mli
+4 -2 metaprl/theories/ocaml/ocaml_df.ml