From 9cb28c30955db553f5e2b7abe7633dec97fa9dae Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 22 Aug 2020 12:51:25 +0200
Subject: Do not write "rename" for arguments in About, since these arguments
 are validated.

---
 vernac/prettyp.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'vernac')

diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index 722a27c432..037ad7db1d 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -320,11 +320,7 @@ let print_arguments ref =
     | Some (UnfoldWhen { nargs; recargs }) -> [], recargs, nargs
     | Some (UnfoldWhenNoMatch { nargs; recargs }) -> [`ReductionDontExposeCase], recargs, nargs
   in
-  let flags, renames = match Arguments_renaming.arguments_names ref with
-    | exception Not_found -> flags, []
-    | [] -> flags, []
-    | renames -> `Rename::flags, renames
-  in
+  let renames = try Arguments_renaming.arguments_names ref with Not_found -> [] in
   let scopes = Notation.find_arguments_scope ref in
   let flags = if needs_extra_scopes ref scopes then `ExtraScopes::flags else flags in
   let impls = Impargs.extract_impargs_data (Impargs.implicits_of_global ref) in
-- 
cgit v1.2.3