From 03f6a1fe5ee4fca81a6b4252fb81c787213ef541 Mon Sep 17 00:00:00 2001 From: Fabian Date: Sat, 16 Sep 2017 21:31:56 +0200 Subject: [PATCH] Use ensure_not_empty_ when vector is known to be non-empty --- src/core/CCVector.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/core/CCVector.ml b/src/core/CCVector.ml index 57f5548b..2d115673 100644 --- a/src/core/CCVector.ml +++ b/src/core/CCVector.ml @@ -156,7 +156,7 @@ let append a b = a.size <- b.size ) else ( - ensure a (a.size + b.size); + ensure_not_empty_ a (a.size + b.size); assert (Array.length a.vec >= a.size + b.size); Array.blit b.vec 0 a.vec a.size b.size; a.size <- a.size + b.size @@ -210,7 +210,7 @@ let append_array a b = a.size <- len_b; ) else ( - ensure a (a.size + len_b); + ensure_not_empty_ a (a.size + len_b); Array.blit b 0 a.vec a.size len_b; a.size <- a.size + len_b )