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.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'kernel/section.ml')

diff --git a/kernel/section.ml b/kernel/section.ml
index 948a967f96..8c36f16799 100644
--- a/kernel/section.ml
+++ b/kernel/section.ml
@@ -45,6 +45,8 @@ let has_poly_univs sec = sec.has_poly_univs
 
 let all_poly_univs sec = sec.all_poly_univs
 
+let map_custom f sec = {sec with sec_custom = f sec.sec_custom}
+
 let find_emap e (cmap, imap) = match e with
 | SecDefinition con -> Cmap.find con cmap
 | SecInductive ind -> Mindmap.find ind imap
-- 
cgit v1.2.3