diff options
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 |