diff options
| author | Matthieu Sozeau | 2014-09-17 11:42:05 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-17 12:37:02 +0200 |
| commit | 9de1edd730eeb3cada742a27a36bc70178eda6d8 (patch) | |
| tree | 341d93576b40d8fc4bb2e6abd6096a69df6b09a6 /proofs | |
| parent | d34e1eed232c84590ddb80d70db9f7f7cf13584a (diff) | |
While resolving typeclass evars in clenv, touch only the ones that appear in the
clenv's value and type, ensuring we don't try to solve unrelated
goals (fixes bug#3633).
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenvtac.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 99ea2300c5..bbf7c27fd9 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -59,15 +59,21 @@ let clenv_pose_dependent_evars with_evars clenv = (RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs))); clenv_pose_metas_as_evars clenv dep_mvs +let clenv_evars clenv value = + let templset = Evar.Set.union (Evarutil.evars_of_term value) + (Evarutil.evars_of_term (clenv_type clenv)) + in fun ev _ -> Evar.Set.mem ev templset + let clenv_refine with_evars ?(with_classes=true) clenv = (** ppedrot: a Goal.enter here breaks things, because the tactic below may solve goals by side effects, while the compatibility layer keeps those useless goals. That deserves a FIXME. *) Proofview.V82.tactic begin fun gl -> let clenv = clenv_pose_dependent_evars with_evars clenv in + let value = clenv_value clenv in let evd' = if with_classes then - let evd' = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars + let evd' = Typeclasses.resolve_typeclasses ~filter:(clenv_evars clenv value) ~fail:(not with_evars) clenv.env clenv.evd in Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals evd' else clenv.evd @@ -75,7 +81,7 @@ let clenv_refine with_evars ?(with_classes=true) clenv = let clenv = { clenv with evd = evd' } in tclTHEN (tclEVARS (Evd.clear_metas evd')) - (refine_no_check (clenv_cast_meta clenv (clenv_value clenv))) gl + (refine_no_check (clenv_cast_meta clenv value)) gl end open Unification |