aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-05-16 00:06:51 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-05-28 15:28:24 +0200
commit4552729b88058946055dddde1533057e25bfc5a9 (patch)
tree38c4c1440c9aa03430b63da175663f96bcf668dd /plugins
parentb053d98fb17d2f46878f49d7adf4839ae632c10b (diff)
Unify pre_env and env
We now have only two notions of environments in the kernel: env and safe_env.
Diffstat (limited to 'plugins')
-rw-r--r--plugins/ltac/evar_tactics.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index fb6be430f..5463893ad 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -52,7 +52,7 @@ let instantiate_tac n c ido =
match ido with
ConclLocation () -> evar_list sigma (pf_concl gl)
| HypLocation (id,hloc) ->
- let decl = Environ.lookup_named_val id (Goal.V82.hyps sigma (sig_it gl)) in
+ let decl = Environ.lookup_named id (pf_env gl) in
match hloc with
InHyp ->
(match decl with