aboutsummaryrefslogtreecommitdiff
path: root/library/library.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/library.ml')
-rw-r--r--library/library.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/library/library.ml b/library/library.ml
index 6edc044a4b..cbd4789532 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -62,7 +62,6 @@ let (raw_extern_module, raw_intern_module) =
let segment_iter f =
let rec apply = function
| sp,Leaf obj -> f (sp,obj)
- | _,ClosedSection (_,mseg) -> iter mseg
| _,OpenedSection _ -> assert false
| _,FrozenState _ -> ()
and iter seg =