From f98de3a79cdf03198705ab5db6c7a1dd8657cb50 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 5 Apr 2013 19:03:30 +0000
Subject: 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
---
 proofs/logic.ml | 1 +
 1 file changed, 1 insertion(+)

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
-- 
cgit v1.2.3