Efficient computation of the names contained in an environment.

12 files changed, 21 insertions, 15 deletions

diff --git a/engine/namegen.ml b/engine/namegen.ml
index 489666852..1dd29e6ea 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -302,7 +302,7 @@ let next_name_away = next_name_away_with_default default_non_dependent_string
 
 let make_all_name_different env sigma =
   (** FIXME: this is inefficient, but only used in printing *)
-  let avoid = ref (Context.Named.to_vars (named_context env)) in
+  let avoid = ref (ids_of_named_context_val (named_context_val env)) in
   let sign = named_context_val env in
   let rels = rel_context env in
   let env0 = reset_with_named_context sign env in
diff --git a/engine/termops.ml b/engine/termops.ml
index e2bdf7238..b7fa2dc4a 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1071,9 +1071,9 @@ let replace_term_gen sigma eq_fun c by_c in_t =
 let replace_term sigma c byc t = replace_term_gen sigma EConstr.eq_constr c byc t
 
 let vars_of_env env =
-  let s =
-    Context.Named.fold_outside (fun decl s -> Id.Set.add (NamedDecl.get_id decl) s)
-      (named_context env) ~init:Id.Set.empty in
+  let s = Environ.ids_of_named_context_val (Environ.named_context_val env) in
+  if List.is_empty (Environ.rel_context env) then s
+  else
   Context.Rel.fold_outside
     (fun decl s -> match RelDecl.get_name decl with Name id -> Id.Set.add id s | _ -> s)
     (rel_context env) ~init:s
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 621a9931d..c3fd8962e 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -101,6 +101,8 @@ let fold_rel_context f env ~init =
 
 let named_context_of_val c = c.env_named_ctx
 
+let ids_of_named_context_val c = Id.Map.domain c.env_named_map
+
 (* [map_named_val f ctxt] apply [f] to the body and the type of
    each declarations.
    *** /!\ ***   [f t] should be convertible with t *)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 377c61de2..2667ad7ca 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -80,6 +80,7 @@ val fold_rel_context :
 val named_context_of_val : named_context_val -> Context.Named.t
 val val_of_named_context : Context.Named.t -> named_context_val
 val empty_named_context_val : named_context_val
+val ids_of_named_context_val : named_context_val -> Id.Set.t
 
 
 (** [map_named_val f ctxt] apply [f] to the body and the type of
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index be1d947d3..d9150a7bb 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -88,7 +88,7 @@ let let_evar name typ =
     let id = match name with
     | Name.Anonymous ->
       let id = Namegen.id_of_name_using_hdchar env sigma typ name in
-      Namegen.next_ident_away_in_goal id (Context.Named.to_vars (Environ.named_context env))
+      Namegen.next_ident_away_in_goal id (Termops.vars_of_env env)
     | Name.Name id -> id
     in
     let (sigma, evar) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index af28e2a6b..08ce72932 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1570,7 +1570,7 @@ let matx_of_eqns env eqns =
   let build_eqn (loc,(ids,lpat,rhs)) =
     let initial_lpat,initial_rhs = lpat,rhs in
     let initial_rhs = rhs in
-    let avoid = Context.Named.to_vars (named_context env) in
+    let avoid = ids_of_named_context_val (named_context_val env) in
     let avoid = List.fold_left (fun accu id -> Id.Set.add id accu) avoid ids in
     let rhs =
       { rhs_env = env;
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index d81b88660..69a49749c 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -221,7 +221,7 @@ let lookup_name_as_displayed env sigma t s =
 	   | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c'))
     | Cast (c,_,_) -> lookup avoid n c
     | _ -> None
-  in lookup (Context.Named.to_vars (named_context env)) 1 t
+  in lookup (Environ.ids_of_named_context_val (Environ.named_context_val env)) 1 t
 
 let lookup_index_as_renamed env sigma t n =
   let rec lookup n d c = match EConstr.kind sigma c with
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index 9fed28bb3..5f12f360b 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -72,7 +72,7 @@ let define_pure_evar_as_product evd evk =
   let open Context.Named.Declaration in
   let evi = Evd.find_undefined evd evk in
   let evenv = evar_env evi in
-  let id = next_ident_away idx (Context.Named.to_vars (evar_context evi)) in
+  let id = next_ident_away idx (Environ.ids_of_named_context_val evi.evar_hyps) in
   let concl = Reductionops.whd_all evenv evd (EConstr.of_constr evi.evar_concl) in
   let s = destSort evd concl in
   let evd1,(dom,u1) =
@@ -127,7 +127,7 @@ let define_pure_evar_as_lambda env evd evk =
   | Prod (na,dom,rng) -> (evd,(na,dom,rng))
   | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd evd typ
   | _ -> error_not_product env evd typ in
-  let avoid = Context.Named.to_vars (evar_context evi) in
+  let avoid = Environ.ids_of_named_context_val evi.evar_hyps in
   let id =
     next_name_away_with_default_using_types "x" na avoid (Reductionops.whd_evar evd dom) in
   let newenv = push_named (LocalAssum (id, dom)) evenv in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 8652a4146..ad1409f5b 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -679,7 +679,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
   let filter1 = evar_filter evi1 in
   let src = subterm_source evk1 evi1.evar_source in
   let ids1 = List.map get_id (named_context_of_val sign1) in
-  let avoid = Context.Named.to_vars (named_context_of_val sign1) in
+  let avoid = Environ.ids_of_named_context_val sign1 in
   let inst_in_sign = List.map mkVar (Filter.filter_list filter1 ids1) in
   let open Context.Rel.Declaration in
   let (sign2,filter2,inst2_in_env,inst2_in_sign,_,evd,_) =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 59cb43302..d52c3932d 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1616,7 +1616,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
   let id =
     let t = match ty with Some t -> t | None -> get_type_of env sigma c in
     let x = id_of_name_using_hdchar (Global.env()) sigma t name in
-    let ids = Context.Named.to_vars (named_context env) in
+    let ids = Environ.ids_of_named_context_val (named_context_val env) in
     if name == Anonymous then next_ident_away_in_goal x ids else
     if mem_named_context_val x (named_context_val env) then
       user_err ~hdr:"Unification.make_abstraction_core"
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index b08051d75..a8ec4d8ca 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -64,7 +64,8 @@ let pf_get_hyp_typ gls id =
   id |> pf_get_hyp gls |> NamedDecl.get_type
 
 let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls)
-let pf_ids_set_of_hyps gls = Context.Named.to_vars (pf_hyps gls)
+let pf_ids_set_of_hyps gls =
+  Environ.ids_of_named_context_val (Environ.named_context_val (pf_env gls))
 
 let pf_get_new_id id gls =
   next_ident_away id (pf_ids_set_of_hyps gls)
@@ -175,8 +176,8 @@ module New = struct
   let pf_ids_set_of_hyps gl =
     (** We only get the identifiers in [hyps] *)
     let gl = Proofview.Goal.assume gl in
-    let hyps = Proofview.Goal.hyps gl in
-    Context.Named.to_vars hyps
+    let env = Proofview.Goal.env gl in
+    Environ.ids_of_named_context_val (Environ.named_context_val env)
 
   let pf_get_new_id id gl =
     let ids = pf_ids_set_of_hyps gl in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4a0525889..d6c24e9cc 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -384,7 +384,9 @@ let rename_hyp repl =
 (**************************************************************)
 
 let fresh_id_in_env avoid id env =
-  next_ident_away_in_goal id (Id.Set.union avoid (Context.Named.to_vars (named_context env)))
+  let avoid' = ids_of_named_context_val (named_context_val env) in
+  let avoid = if Id.Set.is_empty avoid then avoid' else Id.Set.union avoid' avoid in
+  next_ident_away_in_goal id avoid
 
 let fresh_id avoid id gl =
   fresh_id_in_env avoid id (pf_env gl)