From 6d520f47e907010f556ef4ba24715607390460ef Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Fri, 24 Feb 2017 20:13:57 +0100
Subject: Remove a dead exception catching code.

The code was assuming that Proofview.tclFOCUS could raise a
CList.IndexOutOfRange exception but this isn't the case.
The focusing functions already catch this exception and
raises an algebraic exception within the tactic mechanism.
---
 proofs/pfedit.ml | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 80bea0c3b1..b06ea43bdd 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -143,12 +143,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
     in
     (p,status)
   with
-    | Proof_global.NoCurrentProof  -> CErrors.error "No focused proof"
-    | CList.IndexOutOfRange ->
-        match gi with
-	| Vernacexpr.SelectNth i -> let msg = str "No such goal: " ++ int i ++ str "." in
-	                            CErrors.user_err  msg
-        | _ -> assert false
+    Proof_global.NoCurrentProof -> CErrors.error "No focused proof"
 
 let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac)
 
-- 
cgit v1.2.3