diff options
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? *) |