diff options
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index f71719cb9..b590a8c93 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -241,7 +241,7 @@ let print_name_infos ref = let impls = implicits_of_global ref in let scopes = Notation.find_arguments_scope ref in let renames = - try List.hd (Arguments_renaming.arguments_names ref) with Not_found -> [] in + try Arguments_renaming.arguments_names ref with Not_found -> [] in let type_info_for_implicit = if need_expansion (select_impargs_size 0 impls) ref then (* Need to reduce since implicits are computed with products flattened *) @@ -281,7 +281,7 @@ let print_inductive_implicit_args = let print_inductive_renames = print_args_data_of_inductive_ids (fun r -> - try List.hd (Arguments_renaming.arguments_names r) with Not_found -> []) + try Arguments_renaming.arguments_names r with Not_found -> []) ((!=) Anonymous) print_renames_list |