From 73c5ecd3d038b4143910762c0132e147c56a85a2 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Sun, 6 Oct 2013 19:09:35 +0000
Subject: Removing uses of Evar.add in class-related functions.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16852 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/typeclasses_errors.mli | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'pretyping/typeclasses_errors.mli')

diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index a55b9204ef..94bbfce00e 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -25,7 +25,9 @@ type typeclass_error =
   | NotAClass of constr
   | UnboundMethod of global_reference * Id.t located (** Class name, method *)
   | NoInstance of Id.t located * constr list
-  | UnsatisfiableConstraints of evar_map * (existential_key * Evar_kinds.t) option
+  | UnsatisfiableConstraints of
+    evar_map * (existential_key * Evar_kinds.t) option * Evar.Set.t option
+    (** evar map, unresolvable evar, connex component *)
   | MismatchedContextInstance of contexts * constr_expr list * rel_context (** found, expected *)
 
 exception TypeClassError of env * typeclass_error
@@ -36,7 +38,8 @@ val unbound_method : env -> global_reference -> Id.t located -> 'a
 
 val no_instance : env -> Id.t located -> constr list -> 'a
 
-val unsatisfiable_constraints : env -> evar_map -> evar option -> 'a
+val unsatisfiable_constraints : env -> evar_map -> evar option ->
+  Evar.Set.t option -> 'a
 
 val mismatched_ctx_inst : env -> contexts -> constr_expr list -> rel_context -> 'a
 
-- 
cgit v1.2.3