diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenvtac.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 8df0858910..addf12ca13 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -73,11 +73,11 @@ let clenv_pose_dependent_evars with_evars clenv = let clenv_refine with_evars ?(with_classes=true) clenv gls = let clenv = clenv_pose_dependent_evars with_evars clenv in - let evd = Evd.solve_sort_constraints clenv.evd in let evd' = if with_classes then - Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env evd - else evd + Typeclasses.resolve_typeclasses ~fail:(not with_evars) + clenv.env clenv.evd + else clenv.evd in tclTHEN (tclEVARS ( evd')) |