Tracking careless uses of slow name lookup.

2 files changed, 14 insertions, 14 deletions

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
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f47141efb..e93a82e4d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -179,10 +179,10 @@ let introduction ?(check=true) id =
     let gl = Proofview.Goal.assume gl in
     let concl = Proofview.Goal.concl gl in
     let sigma = Tacmach.New.project gl in
-    let hyps = Proofview.Goal.hyps gl in
+    let hyps = named_context_val (Proofview.Goal.env gl) in
     let store = Proofview.Goal.extra gl in
     let env = Proofview.Goal.env gl in
-    let () = if check && mem_named_context id hyps then
+    let () = if check && mem_named_context_val id hyps then
       errorlabstrm "Tactics.introduction"
         (str "Variable " ++ pr_id id ++ str " is already declared.")
     in
@@ -507,7 +507,7 @@ let mutual_fix f n rest j = Proofview.Goal.nf_enter { enter = begin fun gl ->
     let (sp', u')  = check_mutind env sigma n ar in
     if not (eq_mind sp sp') then
       error "Fixpoints should be on the same mutual inductive declaration.";
-    if mem_named_context f (named_context_of_val sign) then
+    if mem_named_context_val f sign then
       errorlabstrm "Logic.prim_refiner"
         (str "Name " ++ pr_id f ++ str " already used in the environment");
     mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth
@@ -560,7 +560,7 @@ let mutual_cofix f others j = Proofview.Goal.nf_enter { enter = begin fun gl ->
   | [] -> sign
   | (f, ar) :: oth ->
     let open Context.Named.Declaration in
-    if mem_named_context f (named_context_of_val sign) then
+    if mem_named_context_val f sign then
       error "Name already used in the environment.";
     mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth
   in
@@ -2782,7 +2782,7 @@ let old_generalize_dep ?(with_let=false) c gl =
   let tothin = List.filter (fun id -> not (Id.List.mem id init_ids)) qhyps in
   let tothin' =
     match kind_of_term c with
-      | Var id when mem_named_context id sign && not (Id.List.mem id init_ids)
+      | Var id when mem_named_context_val id (val_of_named_context sign) && not (Id.List.mem id init_ids)
 	  -> id::tothin
       | _ -> tothin
   in
@@ -2932,8 +2932,8 @@ let unfold_body x =
   let open Context.Named.Declaration in
   Proofview.Goal.enter { enter = begin fun gl ->
   (** We normalize the given hypothesis immediately. *)
-  let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
-  let xval = match Context.Named.lookup x hyps with
+  let env = Proofview.Goal.env (Proofview.Goal.assume gl) in
+  let xval = match Environ.lookup_named x env with
   | LocalAssum _ -> errorlabstrm "unfold_body"
     (pr_id x ++ str" is not a defined hypothesis.")
   | LocalDef (_,xval,_) -> xval
@@ -4355,7 +4355,7 @@ let induction_gen clear_flag isrec with_evars elim
   let cls = Option.default allHypsAndConcl cls in
   let t = typ_of env sigma c in
   let is_arg_pure_hyp =
-    isVar c && not (mem_named_context (destVar c) (Global.named_context()))
+    isVar c && not (mem_named_context_val (destVar c) (Global.named_context_val ()))
     && lbind == NoBindings && not with_evars && Option.is_empty eqname
     && clear_flag == None
     && has_generic_occurrences_but_goal cls (destVar c) env ccl in
@@ -4402,7 +4402,7 @@ let induction_gen_l isrec with_evars elim names lc =
       | [] -> Proofview.tclUNIT ()
       | c::l' ->
 	  match kind_of_term c with
-	    | Var id when not (mem_named_context id (Global.named_context()))
+	    | Var id when not (mem_named_context_val id (Global.named_context_val ()))
 		&& not with_evars ->
 		let _ = newlc:= id::!newlc in
 		atomize_list l'
@@ -4824,7 +4824,7 @@ let abstract_subproof id gk tac =
   let open Context.Named.Declaration in
   Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
   let sigma = Proofview.Goal.sigma gl in
-  let current_sign = Global.named_context()
+  let current_sign = Global.named_context_val ()
   and global_sign = Proofview.Goal.hyps gl in
   let sigma = Sigma.to_evar_map sigma in
   let evdref = ref sigma in
@@ -4832,8 +4832,8 @@ let abstract_subproof id gk tac =
     List.fold_right
       (fun d (s1,s2) ->
         let id = get_id d in
-	if mem_named_context id current_sign &&
-          interpretable_as_section_decl evdref (Context.Named.lookup id current_sign) d
+	if mem_named_context_val id current_sign &&
+          interpretable_as_section_decl evdref (lookup_named_val id current_sign) d
         then (s1,push_named_context_val d s2)
 	else (Context.Named.add d s1,s2))
       global_sign (Context.Named.empty, empty_named_context_val) in