aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/typeclasses_errors.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/typeclasses_errors.mli')
-rw-r--r--pretyping/typeclasses_errors.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 3f0723ad8..b977a1a34 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -42,3 +42,5 @@ val no_instance : env -> identifier located -> constr list -> 'a
val unsatisfiable_constraints : env -> evar_defs -> evar option -> 'a
val mismatched_ctx_inst : env -> contexts -> constr_expr list -> rel_context -> 'a
+
+val unsatisfiable_exception : exn -> bool