From 84c6dc6677ddf527a51eed62adcf8ad5daa77ca1 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 9 Jul 2009 15:32:28 +0000
Subject: Use the proper unification flags in e_exact. This makes exact fail a
 bit more often but respects the spec better. The changes in the stdlib are
 reduced to adding a few explicit [unfold]s in FMapFacts (exact was doing
 conversion with delta on open terms in that case). Also fix a minor bug in
 typeclasses not seeing typeclass evars when their type was a (defined) evar
 itself.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12238 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/typeclasses.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'pretyping/typeclasses.ml')

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 219f9d1277..2f2796f1c6 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -315,17 +315,18 @@ let mark_unresolvables sigma =
     Evd.add evs ev (mark_unresolvable evi))
     sigma Evd.empty
     
-let rec is_class_type c =
+let rec is_class_type evd c =
   match kind_of_term c with
-  | Prod (_, _, t) -> is_class_type t
+  | Prod (_, _, t) -> is_class_type evd t
+  | Evar (e, _) when is_defined evd e -> is_class_type evd (Evarutil.nf_evar evd c)
   | _ -> class_of_constr c <> None
 
-let is_class_evar evi = 
-  is_class_type evi.Evd.evar_concl
+let is_class_evar evd evi = 
+  is_class_type evd evi.Evd.evar_concl
     
 let has_typeclasses evd =
   Evd.fold (fun ev evi has -> has || 
-    (evi.evar_body = Evar_empty && is_class_evar evi && is_resolvable evi))
+    (evi.evar_body = Evar_empty && is_class_evar evd evi && is_resolvable evi))
     evd false
 
 let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false)
-- 
cgit v1.2.3