diff options
| author | aspiwack | 2011-05-13 17:57:41 +0000 |
|---|---|---|
| committer | aspiwack | 2011-05-13 17:57:41 +0000 |
| commit | edcf0d8b8bff399443ddf4cd436185c33bf59829 (patch) | |
| tree | b95d6dd4ae5ccae0114b2fa27c00bcd89f445f78 /plugins/funind/functional_principles_proofs.ml | |
| parent | 1b906116b43f5975fef7bb6f4dfb9589cfe3d6ee (diff) | |
A new mechanism to handle errors.
Instead of the monolitic Cerrors, I introduce a lightweight Errors module
whose error message can be expanded by module introducing exceptions.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14119 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/funind/functional_principles_proofs.ml')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 4f32bbd99d..21ee325398 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -36,7 +36,7 @@ let do_observe_tac s tac g = with e -> let goal = begin try (Printer.pr_goal g) with _ -> assert false end in msgnl (str "observation "++ s++str " raised exception " ++ - Cerrors.explain_exn e ++ str " on goal " ++ goal ); + Errors.print e ++ str " on goal " ++ goal ); raise e;; let observe_tac_stream s tac g = @@ -608,7 +608,7 @@ let my_orelse tac1 tac2 g = try tac1 g with e -> -(* observe (str "using snd tac since : " ++ Cerrors.explain_exn e); *) +(* observe (str "using snd tac since : " ++ Errors.print e); *) tac2 g let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id = |