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 +-
 theories/Vectors/VectorSpec.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

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
diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v
index ed2b56d1f8..5f33836165 100644
--- a/theories/Vectors/VectorSpec.v
+++ b/theories/Vectors/VectorSpec.v
@@ -67,7 +67,7 @@ refine (@Fin.rectS _ _ _); lazy beta; [ intros n v | intros n p H v ].
       (forall v0 : t A (S n), (shiftrepeat v0) [@ Fin.L_R 1 p ] = v0 [@p]) ->
       (shiftrepeat v) [@Fin.L_R 1 (Fin.FS p)] = v [@Fin.FS p]
     |_ => fun _ => @ID end v' with
-  |[] => @id |h :: t => _ end). destruct n0. exact @id. now simpl.
+  |[] => @id |h :: t => _ end). destruct H. exact @id. now simpl.
 Qed.
 
 Lemma shiftrepeat_last A: forall n (v: t A (S n)), last (shiftrepeat v) = last v.
-- 
cgit v1.2.3