diff options
| author | Gaëtan Gilbert | 2019-07-08 13:07:30 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-07-08 13:07:30 +0200 |
| commit | a5e4dd7faa23abd4a4ebe093076484d090a8a47e (patch) | |
| tree | e0de245adb468dc3fe95d9108be749f010457365 /plugins/funind/indfun.ml | |
| parent | 5ecfe31f9d900c6053531f2cb713035407009ba7 (diff) | |
| parent | 07abf9818a6b47bb2c2bd0a8201da9743a0c10b6 (diff) | |
Merge PR #9686: [error] Remove special error printing pre-processing
Reviewed-by: SkySkimmer
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 |