diff options
| author | msozeau | 2009-10-15 02:48:15 +0000 |
|---|---|---|
| committer | msozeau | 2009-10-15 02:48:15 +0000 |
| commit | 4bae5041789fda4d686726d27ea468b227620cd4 (patch) | |
| tree | e1c14add60342cf365bcc1836ea82e824a1bf9e5 | |
| parent | b3c7ac150df37e339aa43dbdb575b3b1a2f00cc1 (diff) | |
Fix bug in typeclass resolution discoverd by Eeelis van der Weegen:
the wrong evar_defs was used when checking if an evar was to be resolved
or not.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12390 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/class_tactics.ml4 | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index a45d9a3b26..c6f29de8b1 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -72,7 +72,7 @@ let evars_to_goals p evm = if evi.evar_body = Evar_empty && Typeclasses.is_resolvable evi (* && not (is_dependent ev evm) *) - && p ev evi then ((ev,evi) :: gls, Evd.add evm' ev (Typeclasses.mark_unresolvable evi)) else + && p evm ev evi then ((ev,evi) :: gls, Evd.add evm' ev (Typeclasses.mark_unresolvable evi)) else (gls, Evd.add evm' ev evi)) evm ([], Evd.empty) in @@ -449,7 +449,7 @@ let _ = let has_undefined p oevd evd = Evd.fold (fun ev evi has -> has || - (evi.evar_body = Evar_empty && p ev evi && + (evi.evar_body = Evar_empty && p oevd ev evi && (try Typeclasses.is_resolvable (Evd.find oevd ev) with _ -> true))) evd false @@ -481,7 +481,8 @@ let resolve_all_evars debug m env p oevd do_split fail = let oevm = oevd in let split = if do_split then split_evars oevd else [Intset.empty] in let p = if do_split then - fun comp ev evi -> (Intset.mem ev comp || not (Evd.mem oevm ev)) && p ev evi + fun comp evd ev evi -> (Intset.mem ev comp || not (Evd.mem oevm ev)) + && p evd ev evi else fun _ -> p in let rec aux n p evd = @@ -519,9 +520,9 @@ let resolve_all_evars debug m env p oevd do_split fail = let resolve_typeclass_evars d p env evd onlyargs split fail = let pred = if onlyargs then - (fun ev evi -> Typeclasses.is_implicit_arg (snd (Evd.evar_source ev evd)) && + (fun evd ev evi -> Typeclasses.is_implicit_arg (snd (Evd.evar_source ev evd)) && Typeclasses.is_class_evar evd evi) - else (fun ev evi -> Typeclasses.is_class_evar evd evi) + else (fun evd ev evi -> Typeclasses.is_class_evar evd evi) in resolve_all_evars d p env pred evd split fail let solve_inst debug mode depth env evd onlyargs split fail = |