[Kernel] Documentation

Credit to Basile Desloges

src/kernel_services/analysis/filter/linear_filter.ml

@@ -149,7 +149,7 @@ module Make (Field : Field.S) = struct
 
   (* Invariant computation. The computation of the sum of all past
      contributions, and in particuler the oldest ones, implies to check
-     is an infinite series converge and to compute its limit. This is done
+     if an infinite series converge and to compute its limit. This is done
      by grouping iterations by pack of size [e] and factorizing the common
      state matrix power. This leads to an infinite geometric series in the
      matrix space. If the spectral radius of this matrix is stricly lower
@@ -267,7 +267,7 @@ module Make (Field : Field.S) = struct
            grouping the infinite sum with our rewritting, we do introduce
            correlations that lead to an underapproximation. Those correlations
            are however ignored through a norm based approach and thus the
-           compution is correct. *)
+           computation is correct. *)
         let scale_to_infinity = Field.(one / (one - spectral_norm)) in
         let old_at_infinity = Matrix.(scale_to_infinity ** old) in
         Matrix.(acc + recent + old_at_infinity)

src/kernel_services/analysis/filter/linear_filter.mli

@@ -55,10 +55,10 @@ module Make (Field : Field.S) : sig
   type 'n source
 
   (** Sources constructor. The inputs are as following :
-      - @param matrix is the source matrix, describing how the current and past
+      - [matrix] is the source matrix, describing how the current and past
         measures are taken into account ;
-      - @param center is the measures center ;
-      - @param deviation is the measures deviation. *)
+      - [center] is the measures center ;
+      - [deviation] is the measures deviation. *)
   val source :
     matrix    : ('n succ, 'm succ) Linear.matrix ->
     center    : Field.scalar ->
@@ -70,9 +70,9 @@ module Make (Field : Field.S) : sig
   type 'n filter
 
   (** Filters constructors. The inputs are as following :
-      - @param center is the filter's center ;
-      - @param state is the filter's state matrix ;
-      - @param sources is the list of the filter's sources. *)
+      - [center] is the filter's center ;
+      - [state] is the filter's state matrix ;
+      - [sources] is the list of the filter's sources. *)
   val create :
     state   : ('n succ, 'n succ) Linear.matrix ->
     center  : 'n succ Linear.vector ->

src/libraries/arithmetic/finite.mli

@@ -22,7 +22,7 @@
 
 open Nat
 
-(** {1 Encoding of finite set in OCaml type system.} *)
+(** Encoding of finite set in OCaml type system. *)
 
 (** The type [n finite] encodes all finite sets of cardinal [n]. It is used by
     the module {!Linear} to represent accesses to vectors and matrices
@@ -34,7 +34,7 @@ type 'n finite
     subset to have an element, its cardinal must be at least one. *)
 val first  : 'n succ finite
 
-(** The call [last n] returns a value encoding the last element of any
+(** [last n] returns a value encoding the last element of any
     finite subset of cardinal [n]. *)
 val last   : 'n succ nat -> 'n succ finite