From bd47a678517a6eeb6b85870f7c50b77733120870 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 30 Jul 2014 18:46:54 +0200
Subject: Add an option to solve typeclass goals generated by apply which can't
 be catched otherwise due to the discrepancy between evars and metas.

---
 pretyping/typeclasses.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'pretyping')

diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index ebc6be45fb..295a092a88 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -99,6 +99,7 @@ val mark_unresolvables : ?filter:evar_filter -> evar_map -> evar_map
 val mark_resolvables   : ?filter:evar_filter -> evar_map -> evar_map
 val mark_resolvable : evar_info -> evar_info
 val is_class_evar : evar_map -> evar_info -> bool
+val is_class_type : evar_map -> types -> bool
 
 val resolve_typeclasses : ?filter:evar_filter -> ?split:bool -> ?fail:bool ->
   env -> evar_map -> evar_map
-- 
cgit v1.2.3