From 39a10cba3d610c6f12438084c5de7c1217c8fe94 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 15 Jun 2018 11:44:32 +0200
Subject: Checking if low-level name printers are used on purpose or not.

In particular we check if really used for internal debugging purpose
or to display a message to the user. In the latter case, we replace it
(when possible) by a higher-level printer (e.g. printing foo instead
of Top.foo). In the former case, we clarify that the use is a
debugging use.

Still not perfect (see a few FIXME).
---
 interp/constrextern.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index ddc0a5c000..3996a1756c 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -102,7 +102,7 @@ let _show_inactive_notations () =
       (function
        | NotationRule (scopt, ntn) ->
          Feedback.msg_notice (pr_notation ntn ++ show_scope scopt)
-       | SynDefRule kn -> Feedback.msg_notice (str (Names.KerName.to_string kn)))
+       | SynDefRule kn -> Feedback.msg_notice (str (string_of_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn))))
       !inactive_notations_table
 
 let deactivate_notation nr =
@@ -135,8 +135,9 @@ let reactivate_notation nr =
                              ++ str "is already active" ++ show_scope scopt ++
   str ".")
     | SynDefRule kn ->
+       let s = string_of_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn) in
        Feedback.msg_warning
-         (str "Notation" ++ spc () ++ str (Names.KerName.to_string kn)
+         (str "Notation" ++ spc () ++ str s
           ++ spc () ++ str "is already active.")
 
 
-- 
cgit v1.2.3