From 22f3c77a4fbd67eb1a453bab8fcc61e6aea508ce Mon Sep 17 00:00:00 2001 From: pboutill Date: Thu, 10 Feb 2011 14:11:04 +0000 Subject: local variables can have implicits locally git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13824 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Vectors/VectorDef.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'theories/Vectors') diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index 150342ee8..0fb6e7acb 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -50,7 +50,7 @@ Definition rectS {A} (P:forall {n}, t A (S n) -> Type) |nil => bas a |_ :: _ => @id end - |cons a (S nn') v => rect a nn' v (rectS_fix _ v) + |cons a (S nn') v => rect a _ v (rectS_fix v) end. (** An induction scheme for 2 vectors of same length *) @@ -78,7 +78,7 @@ match v1 as v1' in t _ n1 end v2' with |[] => @id |h2 :: t2 => fun t1' => - rect _ t1' t2 (rect2_fix _ t1' t2) h1 h2 + rect _ t1' t2 (rect2_fix t1' t2) h1 h2 end t1 end. @@ -222,7 +222,7 @@ schemes *) Definition map {A} {B} (f : A -> B) : forall {n} (v:t A n), t B n := fix map_fix {n} (v : t A n) : t B n := match v with | [] => [] - | a :: v' => (f a) :: (map_fix _ v') + | a :: v' => (f a) :: (map_fix v') end. (** map2 g [x1 .. xn] [y1 .. yn] = [(g x1 y1) .. (g xn yn)] *) @@ -244,7 +244,7 @@ Definition fold_right {A B : Type} (f : A->B->B) := {struct v} : B := match v with | [] => b - | a :: w => f a (fold_right_fix _ w b) + | a :: w => f a (fold_right_fix w b) end. (** fold_right2 g [x1 .. xn] [y1 .. yn] c = g x1 y1 (g x2 y2 .. (g xn yn c) .. ) *) @@ -264,7 +264,7 @@ match v in t _ n0 return t C n0 -> A with |cons vh vn vt => fun w => match w in t _ n1 return match n1 with |0 => @ID |S n => t B n -> A end with |[] => @id - |wh :: wt => fun vt' => fold_left2_fix (f a vh wh) _ vt' wt end vt + |wh :: wt => fun vt' => fold_left2_fix (f a vh wh) vt' wt end vt end. End ITERATORS. -- cgit v1.2.3