diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-13 00:00:49 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-13 00:00:49 +0000 |
| commit | c526b81a9a682edf2270cb544e61fe60355003dc (patch) | |
| tree | 56d5b350997fd29d02fc65b584e6146c81c424b6 /printing | |
| parent | a5aaef33d5cab01177105299a2414c9544860cca (diff) | |
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
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/printer.ml | 3 | ||||
| -rw-r--r-- | printing/printmod.ml | 10 |
2 files changed, 8 insertions, 5 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index e73ccfb35..ea6e79876 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -591,7 +591,8 @@ let pr_assumptionset env s = str (string_of_mp mp ^ "." ^ Label.to_string lab) in let safe_pr_ltype typ = - try str " : " ++ pr_ltype typ with _ -> mt () + try str " : " ++ pr_ltype typ + with e when Errors.noncritical e -> mt () in let fold t typ accu = let (v, a, o, tr) = accu in 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)) |