aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/explainErr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/explainErr.ml')
-rw-r--r--vernac/explainErr.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index f68dcae26..504e7095b 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -66,6 +66,8 @@ let process_vernac_interp_error exn = match fst exn with
wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te)
| Typeclasses_errors.TypeClassError(env, te) ->
wrap_vernac_error exn (Himsg.explain_typeclass_error env te)
+ | Implicit_quantifiers.MismatchedContextInstance(e,c,l,x) ->
+ wrap_vernac_error exn (Himsg.explain_mismatched_contexts e c l x)
| InductiveError e ->
wrap_vernac_error exn (Himsg.explain_inductive_error e)
| Modops.ModuleTypingError e ->