Efficient computation of the names contained in an environment.

5 files changed, 6 insertions, 6 deletions

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"