From b772c323f62b322c9b0a4ab90c7de8b1e2066bae Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 10 Sep 2017 02:21:03 +0200
Subject: Efficient computation of the names contained in an environment.

---
 engine/namegen.ml | 2 +-
 engine/termops.ml | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'engine')

diff --git a/engine/namegen.ml b/engine/namegen.ml
index 489666852d..1dd29e6eae 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 e2bdf72387..b7fa2dc4a4 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
-- 
cgit v1.2.3