diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-13 00:00:53 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-13 00:00:53 +0000 |
| commit | 8d70a84682ded179c461e633c7865486c63e55db (patch) | |
| tree | f18d0b843e390cde0bf3d2ea07280a5a37e825f6 | |
| parent | c526b81a9a682edf2270cb544e61fe60355003dc (diff) | |
Restrict (try...with...) to avoid catching critical exn (part 14)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16291 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/vernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 0f848ad4d..733bd52b9 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -65,7 +65,7 @@ let display_cmd_header loc com = let (start,stop) = Loc.unloc loc in let safe_pr_vernac x = try Ppvernac.pr_vernac x - with e -> str (Printexc.to_string e) in + with e when Errors.noncritical e -> str (Printexc.to_string e) in let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com))) in Pp.pp (str "Chars " ++ int start ++ str " - " ++ int stop ++ |