diff options
| author | Maxime Dénès | 2016-10-28 09:29:25 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-10-28 09:29:25 +0200 |
| commit | 4f65c0370c5fc4163fa961a7fabb8e90fa7c45dd (patch) | |
| tree | 24a84ecb587edb6e14a1e1469f604239b7a6d6c2 /printing/prettyp.ml | |
| parent | d500a684be14b0c781ea4cda0ee02d3c5cdcad81 (diff) | |
| parent | ebb5bd7c2048daa7241bb07d8b53d07e0be27e62 (diff) | |
Merge remote-tracking branch 'github/pr/337' into v8.6
Was PR#337: Fix arguments
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 f71719cb9a..b590a8c930 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 |