diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/namegen.ml | 2 | ||||
| -rw-r--r-- | engine/termops.ml | 6 |
2 files changed, 4 insertions, 4 deletions
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 |