aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/logic.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 818a32cea1..c07b6a8007 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -57,6 +57,8 @@ let rec catchable_exception = function
|NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _
|CannotFindWellTypedAbstraction _
|UnsolvableImplicit _)) -> true
+ | Typeclasses_errors.TypeClassError
+ (_, Typeclasses_errors.UnsatisfiableConstraints _) -> true
| _ -> false
(* Tells if the refiner should check that the submitted rules do not