Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Allow catching of WrongAbstractionType, fixing a regression from 8.4

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16389 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
commit f98de3a79cdf03198705ab5db6c7a1dd8657cb50 1 parent 8b37414
msozeau authored
Showing with 1 addition and 0 deletions.
  1. +1 −0  proofs/logic.ml
View
1  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
Please sign in to comment.
Something went wrong with that request. Please try again.