From b3ab1ea6e75d902e12b2b85bd4827e44eeead1ba Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 5 Jun 2008 09:24:50 +0000
Subject: Correctly catch UnresolvableConstraint exception which is now
 located. Fixes Sophia/Float.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11052 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/class_tactics.ml4 | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 192724b68a..5f8eadece7 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -948,7 +948,8 @@ let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause g
 		  else tclIDTAC
 	      in tclTHENLIST [evartac; rewtac] gl
 	    with 
-	      | TypeClassError (env, (UnsatisfiableConstraints _ as e)) -> 
+	    | Stdpp.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
+	    | TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
 		  tclFAIL 0 (str" setoid rewrite failed: unable to satisfy the rewriting constraints." 
 			      ++ fnl () ++ Himsg.explain_typeclass_error env e) gl)
 (* 	      | Not_found -> *)
-- 
cgit v1.2.3