diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-04 18:08:51 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-04 18:08:51 +0000 |
| commit | 6fea2f181221155535fdd86f67ae10077876ca6d (patch) | |
| tree | f65aa64d360ee5826a516f2cb1fe5b668968cc87 | |
| parent | 84b30df7b5ef9479a89de322bceee5619405d195 (diff) | |
Nicer infered names in refine.
When an existential variable is created, the rel context becomes a named context, and identifiers are given to anonymous variables. Instead of using an identifier based on "H" all the time, use an identifier based on the lower case first letter of the type.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17060 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 c8481bca7..2b28c1a75 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -338,7 +338,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_name_away na avoid in + let id = 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 5f3383616..ed2b56d1f 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. |