diff --git a/doc/interpretation.rst b/doc/interpretation.rst
index 2c91a80ac8e1b3cb900eb5b57d95ef4903a24676..1d17a5c6bd7a78265c5541a0cff53b8e55895d78 100644
--- a/doc/interpretation.rst
+++ b/doc/interpretation.rst
@@ -19,7 +19,7 @@ in the WhyML design and implementation. To quote the author, "[the Why3 team] ha
 
 As CAISAR focuses on artificial intelligence systems, it can
 make some additional assumptions on the nature of the
-inputs, program and users, among the following
+inputs, program and users:
 
 * users will have a basic background on linear algebra, and
   expect CAISAR to reflect this
@@ -65,16 +65,12 @@ Functions
 ~~~~~~~~~
 .. code-block:: whyml
 
-  (** Returns the i-th element of v.
-  TODO: what happens if i > length v ?
-  How do we model matrices? vector of vector? Looks kinda limiting.
-  **)
+  (** Returns the i-th element of v. **)
   function ([]) (v: vector 'a) (i: index) : 'a
 
   function length (v: vector 'a) : int
 
-  (** Returns a vector with the i-th element equals to v1[i] - v2[i].
-  TODO: what happens if length v1 is not length v2? **)
+  (** Returns a vector with the i-th element equals to v1[i] - v2[i]. **)
   function (-) (v1: vector 'a) (v2: vector 'a) : vector 'a
 
   function mapi (v: vector 'a) (f: index -> 'a -> 'b) : vector 'b