From a67cc6941434124465f20b14a1256f2ede31a60e Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 21 Aug 2014 10:11:16 +0200
Subject: Move UnsatisfiableConstraints to a pretype error.

---
 proofs/logic.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'proofs')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index dc8f318598..a7538193b0 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -54,7 +54,8 @@ let is_unification_error = function
 | NoOccurrenceFound _ | CannotUnifyBindingType _
 | ActualTypeNotCoercible _ | UnifOccurCheck _
 | CannotFindWellTypedAbstraction _ | WrongAbstractionType _
-| UnsolvableImplicit _| AbstractionOverMeta _ -> true
+| UnsolvableImplicit _| AbstractionOverMeta _
+| UnsatisfiableConstraints _ -> true
 | _ -> false
 
 let catchable_exception = function
@@ -64,9 +65,7 @@ let catchable_exception = function
   (* reduction errors *)
   | Tacred.ReductionTacticError _ -> true
   (* unification and typing errors *)
-  | PretypeError(_,_, e) -> is_unification_error e || is_typing_error e
-  | Typeclasses_errors.TypeClassError
-      (_, Typeclasses_errors.UnsatisfiableConstraints _) -> true
+  | PretypeError(_,_, e) -> is_unification_error e || is_typing_error e 
   | _ -> false
 
 let error_no_such_hypothesis id = raise (RefinerError (NoSuchHyp id))
-- 
cgit v1.2.3