From 6f9a4b28bca5a218eb31bb7afe9d3dffe01f76f0 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 12 Jun 2013 15:17:05 +0000
Subject: One more fix for rewrite: disallow resolving of the (partial)
 constraints happening silently in w_unify and handle this explicitely. Class
 resolution filters now can test the existential key. Fixes Ergo contrib.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16571 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/typeclasses.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/typeclasses.mli')

diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index c8f41841a6..028e393f2f 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -78,7 +78,7 @@ val is_implicit_arg : Evar_kinds.t -> bool
 val instance_constructor : typeclass -> constr list -> constr option * types
 
 (** Filter which evars to consider for resolution. *)
-type evar_filter = Evar_kinds.t -> bool
+type evar_filter = existential_key -> Evar_kinds.t -> bool
 val all_evars : evar_filter
 val all_goals : evar_filter
 val no_goals : evar_filter
-- 
cgit v1.2.3