diff options
| -rw-r--r-- | pretyping/pretyping.ml | 4 |
1 files changed, 1 insertions, 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) |