Better heuristic for name generation backward compatibility. We fallback

to old behaviour whenever we were in Program mode.

2 files changed, 10 insertions, 2 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index a283286478..780da888e2 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -336,7 +336,15 @@ 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_name_away na avoid in
+        let id =
+          (* ppedrot: we want to infer nicer names for the refine tactic, but
+             keeping at the same time backward compatibility in other code
+             using this function. For now, we only attempt to preserve the
+             old behaviour of Program, but ultimately, one should do something
+             about this whole name generation problem. *)
+          if Flags.is_program_mode () then next_name_away na avoid
+          else next_ident_away (id_of_name_using_hdchar env t 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 5f33836165..ed2b56d1f8 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 H. exact @id. now simpl.
+  |[] => @id |h :: t => _ end). destruct n0. exact @id. now simpl.
 Qed.
 
 Lemma shiftrepeat_last A: forall n (v: t A (S n)), last (shiftrepeat v) = last v.