aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-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