5 files changed, 6 insertions, 6 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 215c850b6f..b0ffc775b5 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -27,7 +27,7 @@ let observe strm =
 let do_observe_tac s tac g =
  try let v = tac g in (* msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); *) v
  with e ->
-   let e = Cerrors.process_vernac_interp_error e in
+   let e = ExplainErr.process_vernac_interp_error e in
    let goal = begin try (Printer.pr_goal g) with _ -> assert false end in
    msg_debug (str "observation "++ s++str " raised exception " ++
 	    Errors.print e ++ str " on goal " ++ goal );
@@ -76,7 +76,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 (Cerrors.process_vernac_interp_error reraise)));
+    then print_debug_queue (Some (fst (ExplainErr.process_vernac_interp_error reraise)));
     iraise reraise
 
 let observe_tac_stream s tac g =
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 85897eceeb..42e4903155 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -195,7 +195,7 @@ END
 
 
 let warning_error names e =
-  let (e, _) = Cerrors.process_vernac_interp_error (e, Exninfo.null) in
+  let (e, _) = ExplainErr.process_vernac_interp_error (e, Exninfo.null) in
   match e with
     | Building_graph e ->
        let names = pr_enum Libnames.pr_reference names in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 6e33af8fbe..18817f504c 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -225,7 +225,7 @@ let prepare_body ((name,_,args,types,_),_) rt =
   (fun_args,rt')
 
 let process_vernac_interp_error e =
-  fst (Cerrors.process_vernac_interp_error (e, Exninfo.null))
+  fst (ExplainErr.process_vernac_interp_error (e, Exninfo.null))
 
 let warn_funind_cannot_build_inversion =
   CWarnings.create ~name:"funind-cannot-build-inversion" ~category:"funind"
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index e0c60d6d5c..26fc88a604 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -72,7 +72,7 @@ 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 = Cerrors.process_vernac_interp_error 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 ));
     iraise reraise;;
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 027fe5677e..62f3071151 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -240,7 +240,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 (Cerrors.process_vernac_interp_error reraise));
+    then print_debug_queue true (fst (ExplainErr.process_vernac_interp_error reraise));
     iraise reraise
 
 let observe_tac s tac g =