diff options
Diffstat (limited to 'plugins/funind/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 2ebbb34e4..6e33af8fb 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 @@ -230,7 +230,7 @@ let process_vernac_interp_error e = 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 |