From c526b81a9a682edf2270cb544e61fe60355003dc Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 13 Mar 2013 00:00:49 +0000 Subject: Restrict (try...with...) to avoid catching critical exn (part 13) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16290 85f007b7-540e-0410-9357-904b9bb8a0f7 --- printing/printmod.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'printing/printmod.ml') diff --git a/printing/printmod.ml b/printing/printmod.ml index fd9b1f200..a3dab2806 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -157,7 +157,8 @@ let rec print_modtype env mp locals mty = let seb1 = Option.default mtb1.typ_expr mtb1.typ_expr_alg in let locals' = (mbid, get_new_id locals (MBId.to_id mbid))::locals in - (try Declaremods.process_module_seb_binding mbid seb1 with _ -> ()); + (try Declaremods.process_module_seb_binding mbid seb1 + with e when Errors.noncritical e -> ()); hov 2 (str "Funsig" ++ spc () ++ str "(" ++ pr_id (MBId.to_id mbid) ++ str ":" ++ print_modtype env mp1 locals seb1 ++ @@ -191,7 +192,8 @@ let rec print_modexpr env mp locals mexpr = match mexpr with (Modops.add_module (Modops.module_body_of_type mp' mty)) env in let typ = Option.default mty.typ_expr mty.typ_expr_alg in let locals' = (mbid, get_new_id locals (MBId.to_id mbid))::locals in - (try Declaremods.process_module_seb_binding mbid typ with _ -> ()); + (try Declaremods.process_module_seb_binding mbid typ + with e when Errors.noncritical e -> ()); hov 2 (str "Functor" ++ spc() ++ str"(" ++ pr_id(MBId.to_id mbid) ++ str ":" ++ print_modtype env mp' locals typ ++ str ")" ++ spc () ++ print_modexpr env' mp locals' mexpr) @@ -244,7 +246,7 @@ let print_module with_body mp = try if !short then raise ShortPrinting; print_module' (Some (Global.env ())) mp with_body me ++ fnl () - with _ -> + with e when Errors.noncritical e -> print_module' None mp with_body me ++ fnl () let print_modtype kn = @@ -255,5 +257,5 @@ let print_modtype kn = (try if !short then raise ShortPrinting; print_modtype' (Some (Global.env ())) kn mtb.typ_expr - with _ -> + with e when Errors.noncritical e -> print_modtype' None kn mtb.typ_expr)) -- cgit v1.2.3