diff options
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 |