From c8198ffd5a042e02e8164a52c3470553b70d55d1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 17 Aug 2018 13:08:50 +0200
Subject: More efficient computation of avoided variables during pretyping.

---
 pretyping/pretyping.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 3b9a8e6a1d..a315376aca 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -68,9 +68,7 @@ type t = {
 }
 
 let get_extra env sigma =
-  let open Context.Named.Declaration in
-  let ids = List.map get_id (named_context env) in
-  let avoid = List.fold_right Id.Set.add ids Id.Set.empty in
+  let avoid = Environ.ids_of_named_context_val (Environ.named_context_val env) in
   Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc)
     (rel_context env) ~init:(empty_csubst, avoid, named_context env)
 
-- 
cgit v1.2.3