diff options
| author | Hugo Herbelin | 2016-06-11 08:30:07 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-06-11 08:32:48 +0200 |
| commit | d095d43f09162f3365392f91ebdd48fcf83d9147 (patch) | |
| tree | 624580df096a42c75f7623cc48629f668ea1b784 | |
| parent | 4de7d7fb63a68b766126ae467be1e9bc00b92948 (diff) | |
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.
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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) = |