aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proof.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proof.ml')
-rw-r--r--proofs/proof.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 2aa620c1d..ef454299e 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -428,7 +428,7 @@ module V82 = struct
in
let env = Evd.evar_filtered_env evi in
let rawc = Constrintern.intern_constr env com in
- let ltac_vars = Pretyping.empty_lvar in
+ let ltac_vars = Glob_ops.empty_lvar in
let sigma = Evar_refiner.w_refine (evk, evi) (ltac_vars, rawc) sigma in
Proofview.Unsafe.tclEVARS sigma
end in