diff options
| author | Hugo Herbelin | 2020-08-27 14:48:15 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-28 15:34:00 +0200 |
| commit | d07d14dfd82cd08564ef0513c23236d73a67664f (patch) | |
| tree | f0584509b4390135114e417a37b0c60c41a289eb /vernac | |
| parent | 4b9a823c03b61034e0fde76716a8623ff68977b0 (diff) | |
About: Add a mention that arguments have been renamed, if ever it is the case.
See https://github.com/coq/coq/pull/12875#issuecomment-679190489.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/prettyp.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 7ceaa5a1bc..8b00484b4a 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -341,7 +341,9 @@ let print_arguments ref = let open Constrexpr in let open Vernacexpr in [Ppvernac.pr_vernac_expr - (VernacArguments (CAst.make (AN qid), impls, moreimpls, flags))] + (VernacArguments (CAst.make (AN qid), impls, moreimpls, flags)) ++ + (if renames = [] then mt () else + fnl () ++ str " (where some original arguments have been renamed)")] let print_name_infos ref = let type_info_for_implicit = |