Remove [obj_sec] mentions from nametab comments

library/nametab.mli

@@ -58,16 +58,15 @@ open Globnames
 *)
 
 (** Object prefix morally contains the "prefix" naming of an object to
-   be stored by [library], where [obj_dir] is the "absolute" path,
-   [obj_mp] is the current "module" prefix and [obj_sec] is the
-   "section" prefix.
+   be stored by [library], where [obj_dir] is the "absolute" path and
+   [obj_mp] is the current "module" prefix.
 
     Thus, for an object living inside [Module A. Section B.] the
    prefix would be:
 
-    [ { obj_dir = "A.B"; obj_mp = "A"; obj_sec = "B" } ]
+    [ { obj_dir = "A.B"; obj_mp = "A"; } ]
 
-    Note that both [obj_dir] and [obj_sec] are "paths" that is to say,
+    Note that [obj_dir] is a "path" that is to say,
    as opposed to [obj_mp] which is a single module name.
 
  *)