diff options
Diffstat (limited to 'parsing/prettyp.ml')
| -rw-r--r-- | parsing/prettyp.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index d3eb40d0..99e10908 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -273,7 +273,9 @@ 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 _ -> []) + (fun r -> + try List.hd (Arguments_renaming.arguments_names r) + with e when Errors.noncritical e -> []) ((<>) Anonymous) print_renames_list @@ -737,7 +739,7 @@ let print_coercions () = let index_of_class cl = try fst (class_info cl) - with _ -> + with e when Errors.noncritical e -> errorlabstrm "index_of_class" (pr_class cl ++ spc() ++ str "not a defined class.") @@ -747,7 +749,7 @@ let print_path_between cls clt = let p = try lookup_path_between_class (i,j) - with _ -> + with e when Errors.noncritical e -> errorlabstrm "index_cl_of_id" (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt ++ str ".") |