diff options
| author | Hugo Herbelin | 2018-06-15 11:44:32 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-23 16:34:32 +0200 |
| commit | 39a10cba3d610c6f12438084c5de7c1217c8fe94 (patch) | |
| tree | 86f3a23f9f6bcafd4810a73b90b6152dc1149db7 /engine | |
| parent | 8c15896b3d3cbfc11f5c493282be3dc1c5c27315 (diff) | |
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).
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/termops.ml | 2 | ||||
| -rw-r--r-- | engine/termops.mli | 8 |
2 files changed, 9 insertions, 1 deletions
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 |