diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2013-11-30 00:20:31 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2013-11-30 00:57:43 +0100 |
| commit | b9b737fee66e954c70bbedbe67517e5b91cc0efb (patch) | |
| tree | 3986c25efe057e4eeb84efdb74a309ec9af6769e /pretyping | |
| parent | a889c1ee209ff16f03f89bf1f8f21faba1522a5d (diff) | |
Tentative fix to recover fresh name generation as it was before
new-tacticals merge. This is essentially a revert of 6fea2f which
broke the sacrosanct backward compatibility of name generation,
thus breaking quite a lot of contribs.
Diffstat (limited to 'pretyping')
| -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 |