From 7cf5f94e772df8632b88088f1cf0ae2287e8f64f Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Tue, 10 Jul 2012 10:08:06 +0000
Subject: Fixes bug 2841 ([Focus 0] gives anomaly).

Now a proper error message is displayed.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15574 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernacentries.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index ebe1e4fbed..d4cacf68b7 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1496,7 +1496,10 @@ let vernac_undoto n =
 let vernac_focus gln =
   let p = Proof_global.give_me_the_proof () in
   let n = match gln with None -> 1 | Some n -> n in
-  Proof.focus focus_command_cond () n p; print_subgoals ()
+  if n = 0 then
+    Errors.error "Invalid goal number: 0. Goal numbering starts with 1."
+  else
+    Proof.focus focus_command_cond () n p; print_subgoals ()
 
   (* Unfocuses one step in the focus stack. *)
 let vernac_unfocus () =
-- 
cgit v1.2.3