aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/himsg.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/himsg.mli')
-rw-r--r--vernac/himsg.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index 5b91f9e68..8945ebadb 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -27,7 +27,7 @@ val explain_typeclass_error : env -> typeclass_error -> Pp.t
val explain_recursion_scheme_error : recursion_scheme_error -> Pp.t
-val explain_refiner_error : refiner_error -> Pp.t
+val explain_refiner_error : env -> Evd.evar_map -> refiner_error -> Pp.t
val explain_pattern_matching_error :
env -> Evd.evar_map -> pattern_matching_error -> Pp.t