diff options
author | Stephane Glondu <steph@glondu.net> | 2013-05-08 17:47:10 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 17:47:10 +0200 |
commit | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (patch) | |
tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /parsing/prettyp.ml | |
parent | bf12eb93f3f6a6a824a10878878fadd59745aae0 (diff) |
Imported Upstream version 8.4pl2dfsgupstream/8.4pl2dfsg
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 ".") |