From a5e035d42a7043bcafe392c8e964ce85558cd319 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 7 Sep 2008 00:10:42 +0000
Subject: More debugging of [Equations], now able to discharge even the heavily
 dependent [noConfusion] definitions in "A Few Constructions on Constructors".
 Now the guardness check is blocking.

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

(limited to 'proofs')

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