diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-17 13:57:13 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-17 13:57:13 +0200 |
| commit | a4ad14610cc0baab46264b179c4b8057f40d52c7 (patch) | |
| tree | 75782f47ebe381d84ea66409569167f9ba229c78 /proofs/clenvtac.ml | |
| parent | 9de1edd730eeb3cada742a27a36bc70178eda6d8 (diff) | |
Revert "While resolving typeclass evars in clenv, touch only the ones that appear in the"
This reverts commit 9de1edd730eeb3cada742a27a36bc70178eda6d8.
Not the right way to do it. The evd shouldn't contain unrelated evars in the first place.
Diffstat (limited to 'proofs/clenvtac.ml')
| -rw-r--r-- | proofs/clenvtac.ml | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index bbf7c27fd..99ea2300c 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -59,21 +59,15 @@ 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:(clenv_evars clenv value) + let evd' = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:(not with_evars) clenv.env clenv.evd in Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals evd' else clenv.evd @@ -81,7 +75,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 value)) gl + (refine_no_check (clenv_cast_meta clenv (clenv_value clenv))) gl end open Unification |