From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 pretyping/typeclasses_errors.ml | 32 ++++++++++++++++++--------------
 1 file changed, 18 insertions(+), 14 deletions(-)

(limited to 'pretyping/typeclasses_errors.ml')

diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 8844baab..1de8b7a5 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: typeclasses_errors.ml 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Names
@@ -24,11 +24,11 @@ open Libnames
 
 type contexts = Parameters | Properties
 
-type typeclass_error = 
+type typeclass_error =
     | NotAClass of constr
     | UnboundMethod of global_reference * identifier located (* Class name, method *)
     | NoInstance of identifier located * constr list
-    | UnsatisfiableConstraints of evar_defs * (evar_info * hole_kind) option
+    | UnsatisfiableConstraints of evar_map * (existential_key * hole_kind) option
     | MismatchedContextInstance of contexts * constr_expr list * rel_context (* found, expected *)
 
 exception TypeClassError of env * typeclass_error
@@ -41,15 +41,19 @@ let unbound_method env cid id = typeclass_error env (UnboundMethod (cid, id))
 
 let no_instance env id args = typeclass_error env (NoInstance (id, args))
 
-let unsatisfiable_constraints env evd ev = 
-  let evd = Evd.undefined_evars evd in
-    match ev with
-    | None ->
-	raise (TypeClassError (env, UnsatisfiableConstraints (evd, None)))
-    | Some ev ->
-	let evi = Evd.find (Evd.evars_of evd) ev in
-	let loc, kind = Evd.evar_source ev evd in
-	  raise (Stdpp.Exc_located (loc, TypeClassError
-	    (env, UnsatisfiableConstraints (evd, Some (evi, kind)))))
-	    
+let unsatisfiable_constraints env evd ev =
+  match ev with
+  | None ->
+      raise (TypeClassError (env, UnsatisfiableConstraints (evd, None)))
+  | Some ev ->
+      let loc, kind = Evd.evar_source ev evd in
+	raise (Stdpp.Exc_located (loc, TypeClassError
+	  (env, UnsatisfiableConstraints (evd, Some (ev, kind)))))
+
 let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m))
+
+let rec unsatisfiable_exception exn =
+  match exn with
+  | TypeClassError (_, UnsatisfiableConstraints _) -> true
+  | Stdpp.Exc_located(_, e) -> unsatisfiable_exception e
+  | _ -> false
-- 
cgit v1.2.3