From d19e8bafe6cc18cc47bbb3e3f7aa0d2d719014c0 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 29 Sep 2017 16:50:49 +0200
Subject: Remove a failwith ""

---
 tactics/tactics.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f1dd61358c..8eaf05f3cb 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1577,11 +1577,11 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ())
   let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in
   let indmv = destMeta sigma (nth_arg sigma i elimclause.templval.rebus) in
   let hypmv =
-    try match List.remove Int.equal indmv (clenv_independent elimclause) with
-      | [a] -> a
-      | _ -> failwith ""
-    with Failure _ -> user_err ~hdr:"elimination_clause"
-          (str "The type of elimination clause is not well-formed.") in
+    match List.remove Int.equal indmv (clenv_independent elimclause) with
+    | [a] -> a
+    | _ -> user_err ~hdr:"elimination_clause"
+             (str "The type of elimination clause is not well-formed.")
+  in
   let elimclause'  = clenv_fchain ~flags indmv elimclause indclause in
   let hyp = mkVar id in
   let hyp_typ = Retyping.get_type_of env sigma hyp in
-- 
cgit v1.2.3