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/termops.ml | |
| 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/termops.ml')
| -rw-r--r-- | engine/termops.ml | 2 |
1 files changed, 2 insertions, 0 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 ")" |