X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FGeneral.v;h=2a1a398b5576d40548733415ced4c084ad3d4c6d;hp=4e73755be3425865f4e3cbaaaf14181f20cfe553;hb=b3214686b18b2d6f6905394494da8d1c17587bdb;hpb=3d4dc42bf3f6e2ad7dc35b14ecb8facdb89e9324

diff --git a/src/General.v b/src/General.v
index 4e73755..2a1a398 100644
--- a/src/General.v
+++ b/src/General.v
@@ -893,7 +893,7 @@ Lemma unleaves_injective : forall T (t1 t2:list T), unleaves t1 = unleaves t2 ->
 
 Lemma fst_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@fst _ _) (vec_zip v1 v2) = v1.
   admit.
-  Qed.
+  Defined.
 
 Lemma snd_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@snd _ _) (vec_zip v1 v2) = v2.
   admit.