diff options
Diffstat (limited to 'lib/pp_control.mli')
| -rw-r--r-- | lib/pp_control.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/pp_control.mli b/lib/pp_control.mli index 2551726df..548b98a7f 100644 --- a/lib/pp_control.mli +++ b/lib/pp_control.mli @@ -42,5 +42,5 @@ val deep_ft : Format.formatter (*s For parametrization through vernacular. *) -val set_depth_boxes : int -> unit -val get_depth_boxes : unit -> int +val set_depth_boxes : int option -> unit +val get_depth_boxes : unit -> int option |