diff options
| author | Hugo Herbelin | 2020-08-22 12:51:25 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-28 15:34:00 +0200 |
| commit | 9cb28c30955db553f5e2b7abe7633dec97fa9dae (patch) | |
| tree | 49aea4f8b9d10405a2b76e6ccfdab7049cae7e74 /vernac | |
| parent | 1a91771fdc26bd0260ff26aceb91070217717d3b (diff) | |
Do not write "rename" for arguments in About, since these arguments are validated.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/prettyp.ml | 6 |
1 files changed, 1 insertions, 5 deletions
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 |