aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/lib.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/library/lib.ml b/library/lib.ml
index 985d9efba8..a4d6aaa221 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -441,7 +441,9 @@ let reset_name (loc,id) =
let is_mod_node = function
| OpenedModule _ | OpenedModtype _ | OpenedSection _
- | ClosedSection _ -> true | _ -> false
+ | ClosedSection _ -> true
+ (* | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE" *)
+ | _ -> false
(* Reset on a module or section name in order to bypass constants with
the same name *)