aboutsummaryrefslogtreecommitdiff
path: root/proofs/proof.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proof.ml')
-rw-r--r--proofs/proof.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml
index e9f93d0c8f..5ab4409f8b 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -434,10 +434,10 @@ module V82 = struct
else
CList.nth evl (n-1)
in
- let env = Evd.evar_filtered_env evi in
+ let env = Evd.evar_filtered_env env evi in
let rawc = intern env sigma in
let ltac_vars = Glob_ops.empty_lvar in
- let sigma = Evar_refiner.w_refine (evk, evi) (ltac_vars, rawc) sigma in
+ let sigma = Evar_refiner.w_refine (evk, evi) (ltac_vars, rawc) env sigma in
Proofview.Unsafe.tclEVARS sigma
end in
let { name; poly } = pr in