diff options
| author | Emilio Jesus Gallego Arias | 2019-03-03 16:49:30 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-07 00:57:28 +0200 |
| commit | 07abf9818a6b47bb2c2bd0a8201da9743a0c10b6 (patch) | |
| tree | 0325550fcf395bad3f4951259202f97db182fbaf /plugins/funind/indfun.ml | |
| parent | ae7fc8bc74289bd8a1eca48c8ca8ecf923888285 (diff) | |
[error] Remove special error printing pre-processing
We remove the special error printing pre-processing in favor of just
calling the standard printers.
Error printing has been a bit complex for a while due to an incomplete
migration to a new printing scheme based on registering exception
printers; this PR should alleviate that by completing the registration
approach.
After this cleanup, it should not be ever necessary for normal
functions to worry a lot about catching errors and re-raising them,
unless they have some very special needs.
This change also allows to consolidate the `explainErr` and `himsg`
modules into one, removing the need to export the error printing
functions. Ideally we would make the contents of `himsg` more
localized, but this can be done in a gradual way.
Diffstat (limited to 'plugins/funind/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 16 |
1 files changed, 3 insertions, 13 deletions
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 |