5 files changed, 7 insertions, 19 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index bf2b4c9122..0efb27e3f0 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -79,7 +79,7 @@ let do_observe_tac s tac g =
   with reraise ->
     let reraise = CErrors.push reraise in
     if not (Stack.is_empty debug_queue)
-    then print_debug_queue (Some (fst (ExplainErr.process_vernac_interp_error reraise)));
+    then print_debug_queue (Some (fst reraise));
     iraise reraise
 
 let observe_tac_stream s tac g =
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index e20d010c71..5f859b3e4b 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -227,7 +227,6 @@ END
 {
 
 let warning_error names e =
-  let (e, _) = ExplainErr.process_vernac_interp_error (e, Exninfo.null) in
   match e with
     | Building_graph e ->
        let names = pr_enum Libnames.pr_qualid names in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 9a9e0b9692..48e3129599 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -244,9 +244,6 @@ let prepare_body ((name,_,args,types,_),_) rt =
   let fun_args,rt' = chop_rlambda_n n rt in
   (fun_args,rt')
 
-let process_vernac_interp_error e =
-  fst (ExplainErr.process_vernac_interp_error (e, Exninfo.null))
-
 let warn_funind_cannot_build_inversion =
   CWarnings.create ~name:"funind-cannot-build-inversion" ~category:"funind"
     (fun e' -> strbrk "Cannot build inversion information" ++
@@ -293,11 +290,9 @@ let derive_inversion fix_names =
         fix_names_as_constant
         lind;
       with e when CErrors.noncritical e ->
-      let e' = process_vernac_interp_error e in
-      warn_funind_cannot_build_inversion e'
+        warn_funind_cannot_build_inversion e
   with e when CErrors.noncritical e ->
-    let e' = process_vernac_interp_error e in
-    warn_funind_cannot_build_inversion e'
+    warn_funind_cannot_build_inversion e
 
 let warn_cannot_define_graph =
   CWarnings.create ~name:"funind-cannot-define-graph" ~category:"funind"
@@ -310,17 +305,13 @@ let warn_cannot_define_principle =
       h 1 names ++ error)
 
 let warning_error names e =
-  let e = process_vernac_interp_error e in
   let e_explain e =
     match e with
       | ToShow e ->
-        let e = process_vernac_interp_error e in
         spc () ++ CErrors.print e
       | _ ->
         if do_observe ()
-        then
-          let e = process_vernac_interp_error e in
-          (spc () ++ CErrors.print e)
+        then (spc () ++ CErrors.print e)
         else mt ()
   in
   match e with
@@ -333,7 +324,6 @@ let warning_error names e =
     | _ -> raise e
 
 let error_error names e =
-  let e = process_vernac_interp_error e in
   let e_explain e =
     match e with
       | ToShow e -> spc () ++ CErrors.print e
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 549f6d42c9..8fa001278b 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -54,9 +54,8 @@ let do_observe_tac s tac g =
     msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v
   with reraise ->
     let reraise = CErrors.push reraise in
-    let e = ExplainErr.process_vernac_interp_error reraise in
     observe (hov 0 (str "observation "++ s++str " raised exception " ++
-             CErrors.iprint e ++ str " on goal" ++ fnl() ++ goal ));
+             CErrors.iprint reraise ++ str " on goal" ++ fnl() ++ goal ));
     iraise reraise;;
 
 let observe_tac s tac g =
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 8d6b85f94d..f4edbda04a 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -210,7 +210,7 @@ let print_debug_queue b e =
     begin
       let lmsg,goal = Stack.pop debug_queue in
       if b then
-        Feedback.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ CErrors.print e) ++ str " on goal" ++ fnl() ++ goal))
+        Feedback.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ CErrors.iprint e) ++ str " on goal" ++ fnl() ++ goal))
       else
         begin
           Feedback.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal));
@@ -237,7 +237,7 @@ let do_observe_tac s tac g =
   with reraise ->
     let reraise = CErrors.push reraise in
     if not (Stack.is_empty debug_queue)
-    then print_debug_queue true (fst (ExplainErr.process_vernac_interp_error reraise));
+    then print_debug_queue true reraise;
     iraise reraise
 
 let observe_tac s tac g =