aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--proofs/logic.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 90014835b9..354935aa8c 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -52,6 +52,7 @@ let rec catchable_exception = function
|NoOccurrenceFound _|CannotUnifyBindingType _
|ActualTypeNotCoercible _|UnifOccurCheck _
|CannotFindWellTypedAbstraction _
+ |WrongAbstractionType _
|UnsolvableImplicit _|AbstractionOverMeta _)) -> true
| Typeclasses_errors.TypeClassError
(_, Typeclasses_errors.UnsatisfiableConstraints _) -> true