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 /plugins/decl_mode/decl_mode.ml | |
| parent | bf12eb93f3f6a6a824a10878878fadd59745aae0 (diff) | |
Imported Upstream version 8.4pl2dfsgupstream/8.4pl2dfsg
Diffstat (limited to 'plugins/decl_mode/decl_mode.ml')
| -rw-r--r-- | plugins/decl_mode/decl_mode.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index 730051c1..da88d48d 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -75,9 +75,9 @@ let mode_of_pftreestate pts = Mode_proof let get_current_mode () = - try + try mode_of_pftreestate (Pfedit.get_pftreestate ()) - with _ -> Mode_none + with e when Errors.noncritical e -> Mode_none let check_not_proof_mode str = if get_current_mode () = Mode_proof then |