From b9b737fee66e954c70bbedbe67517e5b91cc0efb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 30 Nov 2013 00:20:31 +0100
Subject: 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.

---
 pretyping/evarutil.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 08643a1d9a..a283286478 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
-- 
cgit v1.2.3