diff options
| author | msozeau | 2009-07-09 15:32:28 +0000 |
|---|---|---|
| committer | msozeau | 2009-07-09 15:32:28 +0000 |
| commit | 84c6dc6677ddf527a51eed62adcf8ad5daa77ca1 (patch) | |
| tree | dc2517398ee4242e9656c7420a5eb5a3c101d82a /pretyping/typeclasses.ml | |
| parent | 2a596b2f6df4d884aaec99a519044036a4a81596 (diff) | |
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
Diffstat (limited to 'pretyping/typeclasses.ml')
| -rw-r--r-- | pretyping/typeclasses.ml | 11 |
1 files changed, 6 insertions, 5 deletions
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) |