From 9b690c608c2a48b26a8ac94325fe0008d438fb3b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 27 Jul 2015 11:03:11 +0200
Subject: Improving over 26aa224293 in reporting unexpected error during scheme
 creation.

This should actually probably be an anomaly, but I'm unsure the code
for decidability schemes is robust enough to dare it.
---
 toplevel/indschemes.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index f8f062dad6..286d164c42 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -184,9 +184,8 @@ let try_declare_scheme what f internal names kn =
         alarm what internal
           (str "Decidability lemma for mutual inductive types not supported.")
     | e when Errors.noncritical e ->
-	alarm what internal
-	  (str "Unknown exception during scheme creation: "++
-           str (Printexc.to_string e))
+        alarm what internal
+	  (str "Unexpected error during scheme creation: " ++ Errors.print e)
 
 let beq_scheme_msg mind =
   let mib = Global.lookup_mind mind in
-- 
cgit v1.2.3