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 /printing/printer.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 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 67d71332b0..5ca330d377 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -944,9 +944,16 @@ let pr_assumptionset env sigma s = let safe_pr_constant env kn = try pr_constant env kn with Not_found -> + (* FIXME? *) let mp,_,lab = Constant.repr3 kn in str (ModPath.to_string mp) ++ str "." ++ Label.print lab in + let safe_pr_inductive env kn = + try pr_inductive env (kn,0) + with Not_found -> + (* FIXME? *) + MutInd.print kn + in let safe_pr_ltype env sigma typ = try str " : " ++ pr_ltype_env env sigma typ with e when CErrors.noncritical e -> mt () @@ -961,7 +968,7 @@ let pr_assumptionset env sigma s = | Constant kn -> safe_pr_constant env kn ++ safe_pr_ltype env sigma typ | Positive m -> - hov 2 (MutInd.print m ++ spc () ++ strbrk"is positive.") + hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is positive.") | Guarded kn -> hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"is positive.") in |