From d07d14dfd82cd08564ef0513c23236d73a67664f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 27 Aug 2020 14:48:15 +0200
Subject: 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.
---
 vernac/prettyp.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'vernac')

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 =
-- 
cgit v1.2.3