diff options
| author | Maxime Dénès | 2018-09-26 15:36:26 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-26 15:36:26 +0200 |
| commit | 6a48e732577b9ab09d458c7526f599d4528fe2fc (patch) | |
| tree | 66cf1df2a49a7ee2470d13dd46b3ee917cdc00e3 /plugins | |
| parent | 5ced288419aed8a622ed2c267e35d9a174facafc (diff) | |
| parent | 39a10cba3d610c6f12438084c5de7c1217c8fe94 (diff) | |
Merge PR #8534: Checking if low-level name printers are used on purpose or not
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 803d35d07c..b219ee25ca 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -272,6 +272,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 67ffae59cc..9f34df4608 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1298,7 +1298,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? *) |