From 305abd64788e6e5b95869c967f291af61a8d3035 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 26 Nov 2023 23:50:13 -0500 Subject: [PATCH] remove dead code --- src/runtime-services/pbrt_services.ml | 2 -- src/runtime-services/push_stream.ml | 7 ------- src/runtime-services/push_stream.mli | 10 ---------- 3 files changed, 19 deletions(-) delete mode 100644 src/runtime-services/push_stream.ml delete mode 100644 src/runtime-services/push_stream.mli diff --git a/src/runtime-services/pbrt_services.ml b/src/runtime-services/pbrt_services.ml index 59b5179a..1b9b5e7b 100644 --- a/src/runtime-services/pbrt_services.ml +++ b/src/runtime-services/pbrt_services.ml @@ -6,8 +6,6 @@ module Value_mode = struct type stream end -module Push_stream = Push_stream - (** Service stubs, client side *) module Client = struct type _ mode = diff --git a/src/runtime-services/push_stream.ml b/src/runtime-services/push_stream.ml deleted file mode 100644 index 7487943e..00000000 --- a/src/runtime-services/push_stream.ml +++ /dev/null @@ -1,7 +0,0 @@ -type 'a t = { - push: 'a -> unit; - close: unit -> unit; -} - -let push self x = self.push x -let close self = self.close () diff --git a/src/runtime-services/push_stream.mli b/src/runtime-services/push_stream.mli deleted file mode 100644 index d62e8c11..00000000 --- a/src/runtime-services/push_stream.mli +++ /dev/null @@ -1,10 +0,0 @@ -(** Producer end of a stream, into which we can push values *) - -type 'a t = { - push: 'a -> unit; - close: unit -> unit; -} -(** Stream of outgoing values, we can push new ones until we close it *) - -val push : 'a t -> 'a -> unit -val close : _ t -> unit