diff options
Diffstat (limited to 'tactics/class_tactics.ml4')
| -rw-r--r-- | tactics/class_tactics.ml4 | 37 |
1 files changed, 25 insertions, 12 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 42df244d..e063124d 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -634,6 +634,23 @@ let has_undefined p oevd evd = snd (p oevd ev evi)) evd false +(** Revert the resolvability status of evars after resolution, + potentially unprotecting some evars that were set unresolvable + just for this call to resolution. *) + +let revert_resolvability oevd evd = + Evd.fold_undefined + (fun ev evi evm -> + try + if not (Typeclasses.is_resolvable evi) then + let evi' = Evd.find_undefined oevd ev in + if Typeclasses.is_resolvable evi' then + Evd.add evm ev (Typeclasses.mark_resolvable evi) + else evm + else evm + with Not_found -> evm) + evd evd + (** If [do_split] is [true], we try to separate the problem in several components and then solve them separately *) @@ -644,7 +661,7 @@ let resolve_all_evars debug m env p oevd do_split fail = let in_comp comp ev = if do_split then Intset.mem ev comp else true in let rec docomp evd = function - | [] -> evd + | [] -> revert_resolvability oevd evd | comp :: comps -> let p = select_and_update_evars p oevd (in_comp comp) in try @@ -659,24 +676,20 @@ let resolve_all_evars debug m env p oevd do_split fail = docomp evd comps in docomp oevd split -let initial_select_evars onlyargs = - if onlyargs then - (fun evd ev evi -> - Typeclasses.is_implicit_arg (snd (Evd.evar_source ev evd)) - && Typeclasses.is_class_evar evd evi) - else - (fun evd ev evi -> Typeclasses.is_class_evar evd evi) +let initial_select_evars filter evd ev evi = + filter (snd evi.Evd.evar_source) && + Typeclasses.is_class_evar evd evi -let resolve_typeclass_evars debug m env evd onlyargs split fail = +let resolve_typeclass_evars debug m env evd filter split fail = let evd = try Evarconv.consider_remaining_unif_problems ~ts:(Typeclasses.classes_transparent_state ()) env evd with _ -> evd in - resolve_all_evars debug m env (initial_select_evars onlyargs) evd split fail + resolve_all_evars debug m env (initial_select_evars filter) evd split fail -let solve_inst debug depth env evd onlyargs split fail = - resolve_typeclass_evars debug depth env evd onlyargs split fail +let solve_inst debug depth env evd filter split fail = + resolve_typeclass_evars debug depth env evd filter split fail let _ = Typeclasses.solve_instanciations_problem := |