aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/typeclasses_errors.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
-rw-r--r--pretyping/typeclasses_errors.ml6
1 files changed, 6 insertions, 0 deletions
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index fc4362875..6a193e910 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -53,3 +53,9 @@ let unsatisfiable_constraints env evd ev =
(env, UnsatisfiableConstraints (evd, Some (evi, kind)))))
let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m))
+
+let rec unsatisfiable_exception exn =
+ match exn with
+ | TypeClassError (_, UnsatisfiableConstraints _) -> true
+ | Ploc.Exc (_, e) -> unsatisfiable_exception e
+ | _ -> false