diff --git a/src/plugins/dive/build.mli b/src/plugins/dive/build.mli index b4be1c5807da72cd4325b1cbe1841ce99925aa96..0f494984a6d0997f35daef712b920bc30a39017a 100644 --- a/src/plugins/dive/build.mli +++ b/src/plugins/dive/build.mli @@ -38,4 +38,4 @@ val explore_backward : depth:int -> t -> node -> unit val show : t -> node -> unit val hide : t -> node -> unit -val reduce_to_horizon : t -> int option range -> node -> unit +val reduce_to_horizon : t -> range -> node -> unit diff --git a/src/plugins/dive/dive_types.ml b/src/plugins/dive/dive_types.ml index 732043390e4b3e3887231f1d07fedee2fe02e986..057cb6ff6bd11213e0ac951dc846ee0f789c5c8a 100644 --- a/src/plugins/dive/dive_types.ml +++ b/src/plugins/dive/dive_types.ml @@ -76,12 +76,12 @@ type graph_diff = { removed_nodes: node list; } -type 'a range = { - backward: 'a; - forward: 'a; +type range = { + backward: int option; + forward: int option; } type window = { - perception: int option range; (* depth of exploration *) - horizon: int option range; (* hide beyond horizon ; None for infinite *) + perception: range; (* depth of exploration *) + horizon: range; (* hide beyond horizon ; None for infinite *) } diff --git a/src/plugins/dive/server_interface.ml b/src/plugins/dive/server_interface.ml index dc881ea4522292dcecf78611cfa4bf366d1c3bf1..f7280c57840dde2100fbc4298245445f8021b873 100644 --- a/src/plugins/dive/server_interface.ml +++ b/src/plugins/dive/server_interface.ml @@ -69,7 +69,7 @@ let origin_to_locations = function callsites -module Range : Data.S with type t = int option range = +module Range : Data.S with type t = range = struct include Record () @@ -80,7 +80,7 @@ struct let descr = "Parametrization of the exploration range." include (val publish "range" ~descr) - type t = int option range + type t = range let to_json r= default |>