From 16677f3d4e71b2f971ed36bbbc3b95d8908a1b13 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 17 Dec 2013 15:08:06 +0100 Subject: 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. --- proofs/evar_refiner.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs') 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' -- cgit v1.2.3