From 0a1202fae3a8ae8cf651c1b699545a8638ec579f Mon Sep 17 00:00:00 2001 From: aspiwack Date: Sat, 2 Nov 2013 15:34:26 +0000 Subject: 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 --- theories/Vectors/VectorSpec.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'theories/Vectors') 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. -- cgit v1.2.3