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/termops.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'engine/termops.ml')

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