Merge branch 'cerrors-cclosure' into trunk

Was PR#226: CErrors & CClosure

1 files changed, 11 insertions, 11 deletions

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 2ebbb34e4c..18817f504c 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -1,5 +1,5 @@
 open Context.Rel.Declaration
-open Errors
+open CErrors
 open Util
 open Names
 open Term
@@ -225,12 +225,12 @@ 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"
     (fun e' -> strbrk "Cannot build inversion information" ++
-                 if do_observe () then (fnl() ++ Errors.print e') else mt ())
+                 if do_observe () then (fnl() ++ CErrors.print e') else mt ())
 
 let derive_inversion fix_names =
   try
@@ -272,10 +272,10 @@ let derive_inversion fix_names =
 	functional_induction
 	fix_names_as_constant
 	lind;
-      with e when Errors.noncritical e ->
+      with e when CErrors.noncritical e ->
       let e' = process_vernac_interp_error e in
       warn_funind_cannot_build_inversion e'
-  with e when Errors.noncritical e ->
+  with e when CErrors.noncritical e ->
     let e' = process_vernac_interp_error e in
     warn_funind_cannot_build_inversion e'
 
@@ -295,12 +295,12 @@ let warning_error names e =
     match e with
       | ToShow e -> 
 	let e = process_vernac_interp_error e in
-	spc () ++ Errors.print e
+	spc () ++ CErrors.print e
       | _ -> 
 	if do_observe () 
 	then 
 	  let e = process_vernac_interp_error e in 
-	  (spc () ++ Errors.print e) 
+	  (spc () ++ CErrors.print e)
 	else mt ()
   in
   match e with
@@ -316,8 +316,8 @@ let error_error names e =
   let e = process_vernac_interp_error e in
   let e_explain e =
     match e with
-      | ToShow e -> spc () ++ Errors.print e
-      | _ -> if do_observe () then (spc () ++ Errors.print e) else mt ()
+      | ToShow e -> spc () ++ CErrors.print e
+      | _ -> if do_observe () then (spc () ++ CErrors.print e) else mt ()
   in
   match e with
     | Building_graph e ->
@@ -385,7 +385,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
 	Array.iter (add_Function is_general) funs_kn;
 	()
       end
-  with e when Errors.noncritical e ->
+  with e when CErrors.noncritical e ->
     on_error names e
 
 let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
@@ -475,7 +475,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
 	   functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
 	);
       derive_inversion [fname]
-    with e when Errors.noncritical e ->
+    with e when CErrors.noncritical e ->
       (* No proof done *)
       ()
   in