diff options
Diffstat (limited to 'pretyping/evarutil.ml')
-rw-r--r-- | pretyping/evarutil.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 08643a1d9..a28328647 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -336,7 +336,7 @@ let push_rel_context_to_named_context env typ = let (subst, vsubst, _, env) = Context.fold_rel_context (fun (na,c,t) (subst, vsubst, avoid, env) -> - let id = next_ident_away (id_of_name_using_hdchar env t na) avoid in + let id = next_name_away na avoid in match extract_if_neq id na with | Some id0 when not (is_section_variable id0) -> (* spiwack: if [id<>id0], rather than introducing a new |