From 088cdbbb205cc97b0e77f9ccce6ae5e8f3d6541d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 31 Mar 2020 11:30:59 +0200
Subject: Fix #11783 Require in Section

---
 kernel/section.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/section.mli')

diff --git a/kernel/section.mli b/kernel/section.mli
index 89739c7da2..2ebb4564b3 100644
--- a/kernel/section.mli
+++ b/kernel/section.mli
@@ -19,6 +19,9 @@ type 'a t
 val depth : 'a t -> int
 (** Number of nested sections. *)
 
+val map_custom : ('a -> 'a) -> 'a t -> 'a t
+(** Modify the custom data *)
+
 (** {6 Manipulating sections} *)
 
 type section_entry =
-- 
cgit v1.2.3