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 /theories/Vectors | |
| 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
Diffstat (limited to 'theories/Vectors')
| -rw-r--r-- | theories/Vectors/VectorSpec.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |