diff options
Diffstat (limited to 'plugins/funind/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 6e33af8fb..18817f504 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" |