diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2013-12-17 15:08:06 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2013-12-17 15:13:22 +0100 |
| commit | 16677f3d4e71b2f971ed36bbbc3b95d8908a1b13 (patch) | |
| tree | d70ab7e108af307cbd9e996b78e0f9f5e945aa42 /proofs/evar_refiner.ml | |
| parent | fb59652405d0e6a9d1100142d473374cd82ae16b (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/evar_refiner.ml')
| -rw-r--r-- | proofs/evar_refiner.ml | 2 |
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' |