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).
---
 engine/termops.ml  | 2 ++
 engine/termops.mli | 8 +++++++-
 2 files changed, 9 insertions(+), 1 deletion(-)

(limited to 'engine')

diff --git a/engine/termops.ml b/engine/termops.ml
index 156d1370e3..710743e92d 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -49,6 +49,8 @@ let pr_puniverses p u =
   if Univ.Instance.is_empty u then p 
   else p ++ str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)"
 
+(* Minimalistic constr printer, typically for debugging *)
+
 let rec pr_constr c = match kind c with
   | Rel n -> str "#"++int n
   | Meta n -> str "Meta(" ++ int n ++ str ")"
diff --git a/engine/termops.mli b/engine/termops.mli
index b967bb6abb..9ce2db9234 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -311,11 +311,17 @@ val pr_metaset : Metaset.t -> Pp.t
 val pr_evar_universe_context : UState.t -> Pp.t
 val pr_evd_level : evar_map -> Univ.Level.t -> Pp.t
 
-(** debug printer: do not use to display terms to the casual user... *)
+(** Internal hook to register user-level printer *)
 
 val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit
+
+(** User-level printers *)
+
 val print_constr     : constr -> Pp.t
 val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t
+
+(** debug printer: do not use to display terms to the casual user... *)
+
 val print_named_context : env -> Pp.t
 val pr_rel_decl : env -> Constr.rel_declaration -> Pp.t
 val print_rel_context : env -> Pp.t
-- 
cgit v1.2.3