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. --- tactics/leminv.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tactics/leminv.ml') diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 642bf520b..40b600c89 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -202,11 +202,11 @@ let inversion_scheme env sigma t sort dep_option inv_op = tclTHEN intro (onLastHypId inv_op)) pf) in let pfterm = List.hd (Proof.partial_proof pf) in - let global_named_context = Global.named_context () in + let global_named_context = Global.named_context_val () in let ownSign = ref begin fold_named_context (fun env d sign -> - if mem_named_context (get_id d) global_named_context then sign + if mem_named_context_val (get_id d) global_named_context then sign else Context.Named.add d sign) invEnv ~init:Context.Named.empty end in -- cgit v1.2.3