[Kernel] Fix in matrix printer and removing Types modules

src/kernel_services/analysis/filter/finite.ml

@@ -20,13 +20,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-open Nat.Types
+open Nat
 
-module Types = struct
-  type 'n finite = int
-end
-
-open Types
+type 'n finite = int
 
 let first : type n. n succ finite = 0
 let next : type n. n finite -> n succ finite = fun n -> n + 1

src/kernel_services/analysis/filter/finite.mli

@@ -20,10 +20,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-open Nat.Types
+open Nat
 
-module Types : sig type 'n finite end
-open Types
+type 'n finite
 
 val first : 'n succ finite
 val next : 'n finite -> 'n succ finite

src/kernel_services/analysis/filter/linear.ml

@@ -20,8 +20,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-open Nat.Types
-open Finite.Types
+open Nat
+open Finite
 
 
 
@@ -87,13 +87,10 @@ module Space (Field : Field.S) = struct
       fun (M m) -> m.rows, m.cols
 
     let pretty (type n m) fmt (M m : (n, m) matrix) =
-      let open Format in
-      let not_first i = not Finite.(i == first) in
-      let newline fmt i = if not_first i then pp_print_newline fmt () in
-      let row fmt i = fprintf fmt "@[<h>%a@]" Vector.pretty (row i (M m)) in
-      let pp_line fmt i () = newline fmt i ; row fmt i in
-      let pp fmt () = Finite.for_each (pp_line fmt) m.rows () in
-      Format.fprintf fmt "@[<v>%a@]" pp ()
+      let cut i = if not Finite.(i == first) then Format.pp_print_cut fmt () in
+      let row i = Format.fprintf fmt "@[<h>%a@]" Vector.pretty (row i (M m)) in
+      let pretty () = Finite.for_each (fun i () -> cut i ; row i) m.rows () in
+      Format.pp_open_vbox fmt 0 ; pretty () ; Format.pp_close_box fmt ()
 
     let init n m init =
       let rows = Nat.to_int n and cols = Nat.to_int m in

src/kernel_services/analysis/filter/linear.mli

@@ -20,8 +20,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-open Nat.Types
-open Finite.Types
+open Nat
+open Finite
 
 
 

src/kernel_services/analysis/filter/linear_filter.ml

@@ -20,7 +20,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-open Nat.Types
+open Nat
 
 
 

src/kernel_services/analysis/filter/linear_filter.mli

@@ -20,7 +20,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-open Nat.Types
+open Nat
 
 module Make (Field : Field.S) : sig
 

src/kernel_services/analysis/filter/nat.ml

@@ -20,15 +20,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-module Types = struct
-  type zero = |
-  type 'n succ = |
-  type 'n nat = int
-  type positive_or_null = PositiveOrNull : 'n nat -> positive_or_null
-  type strictly_positive = StrictlyPositive : 'n succ nat -> strictly_positive
-end
-
-open Types
+type zero = |
+type 'n succ = |
+type 'n nat = int
+type positive_or_null = PositiveOrNull : 'n nat -> positive_or_null
+type strictly_positive = StrictlyPositive : 'n succ nat -> strictly_positive
 
 let zero : zero nat = 0
 let one  : zero succ nat = 1

src/kernel_services/analysis/filter/nat.mli

@@ -20,15 +20,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-module Types : sig
-  type zero = |
-  type 'n succ = |
-  type 'n nat
-  type positive_or_null = PositiveOrNull : 'n nat -> positive_or_null
-  type strictly_positive = StrictlyPositive : 'n succ nat -> strictly_positive
-end
-
-open Types
+type zero = |
+type 'n succ = |
+type 'n nat
+type positive_or_null = PositiveOrNull : 'n nat -> positive_or_null
+type strictly_positive = StrictlyPositive : 'n succ nat -> strictly_positive
 
 val zero : zero nat
 val one  : zero succ nat