diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:34:26 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:34:26 +0000 |
| commit | 0a1202fae3a8ae8cf651c1b699545a8638ec579f (patch) | |
| tree | 652b6ae0fa3458d114467c31e1fe382bd1b755a3 /theories/Vectors | |
| parent | fe9258c4b228fb086baac7cd3d94207f2c43bb48 (diff) | |
A whole new implemenation of the refine tactic.
It now uses the same algorithm as pretyping does.
This produces pretty weird goal when refining pattern matching terms.
Modification of the pattern matching compilation algorithm are pending, hence I will let it be so for now.
The file Zsqrt_compat.v has two temporary [Admitted] related to this issue.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16973 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Vectors')
| -rw-r--r-- | theories/Vectors/VectorSpec.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v index 2d0a75f32..5f3383616 100644 --- a/theories/Vectors/VectorSpec.v +++ b/theories/Vectors/VectorSpec.v @@ -59,7 +59,7 @@ Qed. Lemma shiftrepeat_nth A: forall n k (v: t A (S n)), nth (shiftrepeat v) (Fin.L_R 1 k) = nth v k. Proof. -refine (@Fin.rectS _ _ _); intros. +refine (@Fin.rectS _ _ _); lazy beta; [ intros n v | intros n p H v ]. revert n v; refine (@caseS _ _ _); simpl; intros. now destruct t. revert p H. refine (match v as v' in t _ m return match m as m' return t A m' -> Type with @@ -67,7 +67,7 @@ refine (@Fin.rectS _ _ _); intros. (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. |