From 07a1de8f9fcff9864e53a090307efa48eca8fe94 Mon Sep 17 00:00:00 2001 From: aspiwack Date: Tue, 17 May 2011 10:31:42 +0000 Subject: Fixes bug in [maximal_unfocus] introduced in r14120. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Fixes bug #2546 ( http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2546­ ). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14130 85f007b7-540e-0410-9357-904b9bb8a0f7 --- proofs/proof_global.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs/proof_global.ml') diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 76aa300aa..780f2eeda 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -300,7 +300,7 @@ let maximal_unfocus k p = begin try while Proof.no_focused_goal p do Proof.unfocus k p done - with Proof.FullyUnfocused -> () + with Proof.FullyUnfocused | Util.UserError _ -> () end -- cgit v1.2.3