From 39f62b3ecf3e5dcadd16b10a81c495a30bd24251 Mon Sep 17 00:00:00 2001
From: pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 25 Mar 2013 00:27:12 +0000
Subject: Normalized type for Vector.map2

fix CoRN but there must be an underlying bug ...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16355 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Vectors/VectorDef.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'theories/Vectors')

diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 38675f31e..8f672deda 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -212,7 +212,8 @@ Definition map {A} {B} (f : A -> B) : forall {n} (v:t A n), t B n :=
   end.
 
 (** map2 g [x1 .. xn] [y1 .. yn] = [(g x1 y1) .. (g xn yn)] *)
-Definition map2 {A B C} (g:A -> B -> C) :=
+Definition map2 {A B C} (g:A -> B -> C) :
+  forall (n : nat), t A n -> t B n -> t C n :=
 @rect2 _ _ (fun n _ _ => t C n) (nil C) (fun _ _ _ H a b => (g a b) :: H).
 Global Arguments map2 {A B C} g {n} v1 v2.
 
-- 
cgit v1.2.3