diff options
| author | herbelin | 2006-09-01 12:51:06 +0000 |
|---|---|---|
| committer | herbelin | 2006-09-01 12:51:06 +0000 |
| commit | ff6061b2ee59a64b652f57051c37bbc8e48d4d29 (patch) | |
| tree | 75868adf1430b06358e0adc814b9673524a14a9a /lib | |
| parent | 3a59869620ab78ba4fc764f6f6a848fbeb2abaa4 (diff) | |
Force évaluation 'naturelle' de list_map2_i et list_map3 de gauche à droite
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9112 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/util.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/util.ml b/lib/util.ml index 08b85759a2..e18d13cb60 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -194,7 +194,7 @@ let list_map_i f = let list_map2_i f i l1 l2 = let rec map_i i = function | ([], []) -> [] - | ((h1::t1), (h2::t2)) -> (f i h1 h2) :: (map_i (succ i) (t1,t2)) + | ((h1::t1), (h2::t2)) -> let v = f i h1 h2 in v :: map_i (succ i) (t1,t2) | (_, _) -> invalid_arg "map2_i" in map_i i (l1,l2) @@ -202,7 +202,7 @@ let list_map2_i f i l1 l2 = let list_map3 f l1 l2 l3 = let rec map = function | ([], [], []) -> [] - | ((h1::t1), (h2::t2), (h3::t3)) -> (f h1 h2 h3) :: (map (t1,t2,t3)) + | ((h1::t1), (h2::t2), (h3::t3)) -> let v = f h1 h2 h3 in v::map (t1,t2,t3) | (_, _, _) -> invalid_arg "map3" in map (l1,l2,l3) |