From edb3302188af4b5b75111339e3f466a6ec09aef2 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 12 Mar 2015 17:46:35 +0100
Subject: Declarative mode: make it so that unfocussing can only be done for
 closed subproofs.

The front-end is supposed to take care of that, but it may help to catch bugs.
---
 plugins/decl_mode/decl_mode.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index da41cd86db..07df7c7f09 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -96,7 +96,7 @@ let get_goal_stack pts =
 
 
 let proof_focus = Proof.new_focus_kind ()
-let proof_cond = Proof.no_cond proof_focus
+let proof_cond = Proof.done_cond proof_focus
 
 let focus p =
   let inf = get_goal_stack p in
-- 
cgit v1.2.3