diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenvtac.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index f368ed3791..b1dc7c8961 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -77,8 +77,11 @@ let clenv_pose_dependent_evars with_evars clenv = let clenv_refine with_evars clenv gls = let clenv = clenv_expand_metas clenv in let clenv = clenv_pose_dependent_evars with_evars clenv in + let evd' = Typeclasses.resolve_typeclasses ~fail:(not with_evars) + clenv.env clenv.evd + in tclTHEN - (tclEVARS (evars_of clenv.evd)) + (tclEVARS (evars_of evd')) (refine (clenv_value_cast_meta clenv)) gls |