diff --git a/src/kernel_services/analysis/filter/finite.ml b/src/kernel_services/analysis/filter/finite.ml
index 11af2a7281b5adf487308c437fb7d48574132323..e80796ae2451afb447d8ded1cfa6dae1640609eb 100644
--- a/src/kernel_services/analysis/filter/finite.ml
+++ b/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
diff --git a/src/kernel_services/analysis/filter/finite.mli b/src/kernel_services/analysis/filter/finite.mli
index ed5e8b695cb71617119e9266170f54bed20b6626..007fe137694f5262a72d27a054c3b094c22cf690 100644
--- a/src/kernel_services/analysis/filter/finite.mli
+++ b/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
diff --git a/src/kernel_services/analysis/filter/linear.ml b/src/kernel_services/analysis/filter/linear.ml
index b4a6430d512d7215da5ad8522901256990466f74..72df26f0c6e5a3e7ecce2ad97c492a00cfdab60a 100644
--- a/src/kernel_services/analysis/filter/linear.ml
+++ b/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
diff --git a/src/kernel_services/analysis/filter/linear.mli b/src/kernel_services/analysis/filter/linear.mli
index 8437815b75ab4ae223d14f01eae8334d18272356..7c4ee980aadda61ec74e8fd096595dcebf9aaed8 100644
--- a/src/kernel_services/analysis/filter/linear.mli
+++ b/src/kernel_services/analysis/filter/linear.mli
@@ -20,8 +20,8 @@
(* *)
(**************************************************************************)
-open Nat.Types
-open Finite.Types
+open Nat
+open Finite
diff --git a/src/kernel_services/analysis/filter/linear_filter.ml b/src/kernel_services/analysis/filter/linear_filter.ml
index 8bfad7c20c61d3dcbcafe3af9ebfeff4feb66314..4a32b30dd04ea46a516445dee74897462a3a6252 100644
--- a/src/kernel_services/analysis/filter/linear_filter.ml
+++ b/src/kernel_services/analysis/filter/linear_filter.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-open Nat.Types
+open Nat
diff --git a/src/kernel_services/analysis/filter/linear_filter.mli b/src/kernel_services/analysis/filter/linear_filter.mli
index 3170b118f2e22f94b6a6601725eeac3f3779a7f4..6a16b9b8f5bfa92eb8dae0f4a619a38cc14aab72 100644
--- a/src/kernel_services/analysis/filter/linear_filter.mli
+++ b/src/kernel_services/analysis/filter/linear_filter.mli
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-open Nat.Types
+open Nat
module Make (Field : Field.S) : sig
diff --git a/src/kernel_services/analysis/filter/nat.ml b/src/kernel_services/analysis/filter/nat.ml
index 3f9705c9aa325a9658870a01704da2e2cf12aae1..28e197482e85b7fad514d2dcec7c6f425506cee1 100644
--- a/src/kernel_services/analysis/filter/nat.ml
+++ b/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
diff --git a/src/kernel_services/analysis/filter/nat.mli b/src/kernel_services/analysis/filter/nat.mli
index d3d6cf83feac5f51a9dc5fd96bb3ea53055be0d4..a6d8894dd8c9d0fe200cb778062e9adb622c680f 100644
--- a/src/kernel_services/analysis/filter/nat.mli
+++ b/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