diff --git a/src/kernel_services/analysis/filter/linear_filter.mli b/src/kernel_services/analysis/filter/linear_filter.mli
index e22d3f7bfb2f7202b14fd567062382b6b24f825b..352c681ada85a88ada7861f43dc93fdb57ea658f 100644
--- a/src/kernel_services/analysis/filter/linear_filter.mli
+++ b/src/kernel_services/analysis/filter/linear_filter.mli
@@ -26,17 +26,19 @@ open Finite
 (* A filter corresponds to the recursive equation
    X[k + 1] = AX[k] + Bε[k + 1] + C where :
    - n is the filter's order and m its number of inputs ;
-   - X[k]∈ ℝ^n is the filter's state at iteration [k] ;
-   - ε[k]∈ ℝ^m is the filters's inputs at iteration [k] ;
-   - A∈ ℝ^(n×n) is the filter's state matrix ;
-   - B∈ ℝ^(n×m) is the filter's input matrix ;
-   - C∈ ℝ^n is the filter's center.
+   - X[k] ∈ ℝ^n is the filter's state at iteration [k] ;
+   - ε[k] ∈ ℝ^m is the filters's inputs at iteration [k] ;
+   - A ∈ ℝ^(n×n) is the filter's state matrix ;
+   - B ∈ ℝ^(n×m) is the filter's input matrix ;
+   - C ∈ ℝ^n is the filter's center.
 
    The goal of this module is to compute filters invariants, i.e bounds for
    each of the filter's state dimensions when the iterations goes to infinity.
    To do so, it only suppose that, at each iteration, each input εi is bounded
    by [-λi .. λi]. Each input is thus supposed centered around zero but each
-   one can have different bounds. *)
+   one can have different bounds.
+
+   {!Linear_filter_test} is an example using this module. *)
 module Make (Field : Field.S) : sig
 
   module Linear : module type of Linear.Space (Field)
@@ -71,7 +73,7 @@ module Make (Field : Field.S) : sig
      lower than one. For the filter to converge, there must exist an α such as,
      for every β greater than α, ||A^β|| < 1 with A the filter's state matrix.
      As such, the search does not have to find α, but instead any exponent such
-     as the property is satisfies. As the computed invariant will be more
+     as the property is satisfied. As the computed invariant will be more
      precise with a larger exponent, the computation always uses [k], the
      largest authorized exponent, and thus only check that indeed ||A^k|| < 1.
      If the property is not verified, the function returns None as it cannot
diff --git a/src/kernel_services/analysis/filter/linear_filter_test.ml b/src/kernel_services/analysis/filter/linear_filter_test.ml
index 6634aef53e7e765ef4fae15370c20c7d38895c1d..f239d3adbeefad5443c3761cb5adb613c2516253 100644
--- a/src/kernel_services/analysis/filter/linear_filter_test.ml
+++ b/src/kernel_services/analysis/filter/linear_filter_test.ml
@@ -20,8 +20,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-
-
 module Rational = struct
 
   type scalar = Q.t
@@ -80,6 +78,10 @@ let pretty_invariant order fmt = function
 
 
 
+(* Invariant computation for the filter:
+     X = 0.68 * X - 0.68 * Y + E1;
+     Y = 0.68 * X + 0.68 * Y + E2;
+   with E1 ∈ [-1 .. 1] and E2 ∈ [-1 .. 1]. *)
 module Circle = struct
 
   let order = Nat.(succ one)
@@ -106,6 +108,10 @@ end
 
 
 
+(* Invariant computation for the filter:
+     X = 1.5 * X - 0.7 * Y + E + 1;
+     Y = X + 1;
+   with E ∈ [-0.1 .. 0.1]. *)
 module Simple = struct
 
   let order = Nat.(succ one)
diff --git a/src/kernel_services/analysis/filter/linear_filter_test.mli b/src/kernel_services/analysis/filter/linear_filter_test.mli
index cc9eb1f5468dd841eee7e8ca15071a461d95b5ac..e973f651b1aef8f89f6fc9c1e2a110da2801685f 100644
--- a/src/kernel_services/analysis/filter/linear_filter_test.mli
+++ b/src/kernel_services/analysis/filter/linear_filter_test.mli
@@ -20,4 +20,5 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(** Tests the Linear_filter module: invariant computation of filters. *)
 val run : unit -> unit