aboutsummaryrefslogtreecommitdiff
path: root/kernel/section.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/section.ml')
-rw-r--r--kernel/section.ml2
1 files changed, 2 insertions, 0 deletions
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