Merge PR #17906: Ensure that About on a section name do not fail with…

… an anomaly

Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>

kernel/names.ml

@@ -285,6 +285,8 @@ module ModPath = struct
     | MPbound uid -> MBId.to_string uid
     | MPdot (mp,l) -> to_string mp ^ "." ^ Label.to_string l
 
+  let print mp = str (to_string mp)
+
   let rec debug_to_string = function
     | MPfile sl -> DirPath.to_string sl
     | MPbound uid -> MBId.debug_to_string uid

kernel/names.mli

@@ -264,7 +264,10 @@ sig
   val dp : t -> DirPath.t
 
   val to_string : t -> string
-  (** Encode as a string (not to be used for user-facing messages). *)
+  (** Converts a identifier into an string. *)
+
+  val print : t -> Pp.t
+  (** Pretty-printer. *)
 
   val debug_to_string : t -> string
   (** Same as [to_string], but outputs extra information related to debug. *)

test-suite/output/Nametab.out

@@ -37,3 +37,5 @@ Module Nametab.Q.N
 Module Nametab.Q.N (shorter name to refer to it in current context is Q.N)
 Module Nametab.Q
 Module Nametab.Q (shorter name to refer to it in current context is Q)
+No object of basename T
+Open Section Nametab.T

test-suite/output/Nametab.v

@@ -46,3 +46,9 @@ Import Q.N.
 
 (* OK  *) Locate Module Q.
 (* OK  *) Locate Module Nametab.Q.
+
+(* A slightly different request *)
+Section T.
+Locate T.
+About T.
+End T.

vernac/prettyp.ml

@@ -450,11 +450,11 @@ let pr_located_qualid = function
       let s,mp =
         let open Nametab in
         let open GlobDirRef in match dir with
-        | DirOpenModule mp -> "Open Module", mp
-        | DirOpenModtype mp -> "Open Module Type", mp
-        | DirOpenSection _ -> anomaly (Pp.str"Sections are not locatable")
+        | DirOpenModule mp -> "Open Module", ModPath.print mp
+        | DirOpenModtype mp -> "Open Module Type", ModPath.print mp
+        | DirOpenSection dir -> "Open Section", DirPath.print dir
       in
-      str s ++ spc () ++ str (ModPath.to_string mp)
+      str s ++ spc () ++ mp
   | Module mp ->
     str "Module" ++ spc () ++ DirPath.print (Nametab.dirpath_of_module mp)
   | ModuleType mp ->