diff options
| author | Pierre-Marie Pédrot | 2013-11-30 00:20:31 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2013-11-30 00:57:43 +0100 |
| commit | b9b737fee66e954c70bbedbe67517e5b91cc0efb (patch) | |
| tree | 3986c25efe057e4eeb84efdb74a309ec9af6769e | |
| 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.
| -rw-r--r-- | pretyping/evarutil.ml | 2 | ||||
| -rw-r--r-- | 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. |