aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/discharge.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/discharge.ml')
-rw-r--r--toplevel/discharge.ml3
1 files changed, 1 insertions, 2 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index a29fad5a7..f621e5bee 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -275,8 +275,7 @@ let rec process_object (ccitab, objtab, modtab as tabs) = function
| sp,ClosedSection (export,_,seg,contents) ->
let id = string_of_id (basename sp) in
(ccitab, objtab, Stringmap.add id contents modtab)
- | _,(OpenedSection _ | FrozenState _ | Module _) ->
- anomaly "Should not occur in a closed section"
+ | _,(OpenedSection _ | FrozenState _ | Module _) -> tabs
and module_contents seg =
let ccitab, objtab, modtab =