From d55818c7da468ce1c7c9644cb63f68f7561a17bc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 9 Sep 2016 13:29:28 +0200 Subject: Tracking careless uses of slow name lookup. --- proofs/tacmach.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'proofs/tacmach.ml') diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 50984c48e..ba22db083 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -191,9 +191,9 @@ module New = struct next_ident_away id ids let pf_get_hyp id gl = - let hyps = Proofview.Goal.hyps gl in + let hyps = Proofview.Goal.env gl in let sign = - try Context.Named.lookup id hyps + try Environ.lookup_named id hyps with Not_found -> raise (RefinerError (NoSuchHyp id)) in sign -- cgit v1.2.3