From d095d43f09162f3365392f91ebdd48fcf83d9147 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 11 Jun 2016 08:30:07 +0200
Subject: Fixing a try with in apply that has become too weak in 8.5.

Don't know however what should be the right guard to this try. Now
using catchable_exception, but even in 8.4, Failure was caught, which
is strange.
---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4562e25184..b1df1f5aa4 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1501,7 +1501,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind))
         if n<0 then error "Applied theorem has not enough premisses.";
         let clause = make_clenv_binding_apply env sigma (Some n) (c,thm_ty) lbind in
         Clenvtac.res_pf clause ~with_evars ~flags
-      with UserError _ as exn ->
+      with exn when catchable_exception exn ->
         Proofview.tclZERO exn
     in
     let rec try_red_apply thm_ty (exn0, info) =
-- 
cgit v1.2.3