From be496912193961d9a230dae5b24e4fb7d8cbc042 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 7 Jun 2011 11:14:24 +0000
Subject: Catch AbstractionOverMeta as a unification failure in
 precatchable_exception. Allows rewrite H in * |- to work in case a rewrite
 throws this exception.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14166 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/logic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 2835eb5429..b482628b90 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -57,7 +57,7 @@ let rec catchable_exception = function
   | PretypeError(_,_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _
 		   |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _
 		   |CannotFindWellTypedAbstraction _|OccurCheck _
-		   |UnsolvableImplicit _)) -> true
+		   |UnsolvableImplicit _|AbstractionOverMeta _)) -> true
   | Typeclasses_errors.TypeClassError
       (_, Typeclasses_errors.UnsatisfiableConstraints _) -> true
   | _ -> false
-- 
cgit v1.2.3