From edcf0d8b8bff399443ddf4cd436185c33bf59829 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Fri, 13 May 2011 17:57:41 +0000
Subject: 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
---
 plugins/funind/functional_principles_proofs.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/funind/functional_principles_proofs.ml')

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 =
-- 
cgit v1.2.3