aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2013-12-17 15:08:06 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2013-12-17 15:13:22 +0100
commit16677f3d4e71b2f971ed36bbbc3b95d8908a1b13 (patch)
treed70ab7e108af307cbd9e996b78e0f9f5e945aa42 /proofs
parentfb59652405d0e6a9d1100142d473374cd82ae16b (diff)
Removing the need of evarmaps in constr internalization.
Actually, this was wrong, as evars should not appear until interpretation. Evarmaps were only passed around uselessly, and often fed with dummy or irrelevant values.
Diffstat (limited to 'proofs')
-rw-r--r--proofs/evar_refiner.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 36ba80202..8c2776789 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -63,7 +63,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
let instantiate_pf_com evk com sigma =
let evi = Evd.find sigma evk in
let env = Evd.evar_filtered_env evi in
- let rawc = Constrintern.intern_constr sigma env com in
+ let rawc = Constrintern.intern_constr env com in
let ltac_vars = (Id.Map.empty, Id.Map.empty) in
let sigma' = w_refine (evk, evi) (ltac_vars, rawc) sigma in
sigma'