diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenvtac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index addf12ca13..c3e6e3d87c 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -80,7 +80,7 @@ let clenv_refine with_evars ?(with_classes=true) clenv gls = else clenv.evd in tclTHEN - (tclEVARS ( evd')) + (tclEVARS evd') (refine (clenv_cast_meta clenv (clenv_value clenv))) gls |