diff options
Diffstat (limited to 'kernel/section.ml')
| -rw-r--r-- | kernel/section.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/section.ml b/kernel/section.ml index babd9fe7a1..a1242f0faf 100644 --- a/kernel/section.ml +++ b/kernel/section.ml @@ -43,6 +43,8 @@ let empty = [] let is_empty = List.is_empty +let depth = List.length + let has_poly_univs = function | [] -> false | sec :: _ -> sec.has_poly_univs |