Removed [until_finite], which was now unused.

src/CompletedNat.ml

@@ -48,13 +48,6 @@ let min_lazy p1 p2 =
   | _ ->
       min p1 (p2())
 
-let until_finite p1 p2 =
-  match p1 with
-  | Finite _ ->
-      p1
-  | Infinity ->
-      p2()
-
 let add p1 p2 =
   match p1, p2 with
   | Finite i1, Finite i2 ->

src/CompletedNat.mli

@@ -16,6 +16,4 @@ val add: t -> t -> t
 val min_lazy: t -> (unit -> t) -> t
 val add_lazy: t -> (unit -> t) -> t
 
-val until_finite: t -> (unit -> t) -> t
-
 val print: t -> string

src/CompletedNatWitness.ml

@@ -59,17 +59,6 @@ let min_cutoff p1 p2 =
       (* Pass [max_int] to indicate no cutoff. *)
       p2 max_int
 
-(* [until_finite] can be viewed as a variant of [min_lazy] where
-   we are happy as soon as we find a finite value. It can be viewed
-   as a minimum operation for the partial ordering where [Infinity]
-   is above everyone and everyone else is incomparable. *)
-let until_finite p1 p2 =
-  match p1 with
-  | Finite _ ->
-      p1
-  | Infinity ->
-      p2()
-
 let add p1 p2 =
   match p1, p2 with
   | Finite (i1, xs1), Finite (i2, xs2) ->

src/CompletedNatWitness.mli

@@ -24,8 +24,6 @@ val add_lazy: 'a t -> (unit -> 'a t) -> 'a t
 val min_cutoff: 'a t -> (int -> 'a t) -> 'a t
 val add_cutoff: (* cutoff: *) int -> 'a t -> (int -> 'a t) -> 'a t
 
-val until_finite: 'a t -> (unit -> 'a t) -> 'a t
-
 val print: ('a -> string) -> 'a t -> string
 val to_int: 'a t -> int
 val extract: 'a t -> 'a list