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 /plugins | |
| 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 'plugins')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 2 |
2 files changed, 3 insertions, 1 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 4357689ee2..89353a3c3f 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -271,6 +271,8 @@ let string_of_genarg_arg (ArgumentType arg) = in pr_sequence pr prods with Not_found -> + (* FIXME: This key, moreover printed with a low-level printer, + has no meaning user-side *) KerName.print key let pr_alias_gen pr_gen lev key l = diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 71da6c7667..e551ca4148 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1297,7 +1297,7 @@ and tactic_of_value ist vle = match appl with UnnamedAppl -> "An unnamed user-defined tactic" | GlbAppl apps -> - let nms = List.map (fun (kn,_) -> Names.KerName.to_string kn) apps in + let nms = List.map (fun (kn,_) -> string_of_qualid (Tacenv.shortest_qualid_of_tactic kn)) apps in match nms with [] -> assert false | kn::_ -> "The user-defined tactic \"" ^ kn ^ "\"" (* TODO: when do we not have a singleton? *) |