aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/proof.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 04e707cd6..f5ff35eeb 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -432,7 +432,7 @@ module V82 = struct
CList.nth evl (n-1)
in
let env = Evd.evar_filtered_env evi in
- let rawc = Constrintern.intern_constr env com in
+ let rawc = Constrintern.intern_constr env sigma com 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