From ef79db4628963c46ae66fe25f3e2aeea6db8c2e7 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 22 Feb 2016 17:35:34 +0100
Subject: Guard "catch all" exception handler using Errors.noncritical

---
 mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 3 ++-
 mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4  | 3 ++-
 2 files changed, 4 insertions(+), 2 deletions(-)

(limited to 'mathcomp/ssreflect/plugin')

diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
index f0b6306..0d2326f 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
@@ -3872,7 +3872,8 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl =
       (mkApp (compose_lam l c, Array.of_list (mkRel 1 :: mkRels n)))
   in
   pp(lazy(str"after: " ++ pr_constr oc));
-  try applyn ~with_evars ~with_shelve:true ?beta n oc gl with _ -> raise dependent_apply_error
+  try applyn ~with_evars ~with_shelve:true ?beta n oc gl
+  with e when Errors.noncritical e -> raise dependent_apply_error
 
 let pf_fresh_inductive_instance ind gl =
   let sigma, env, it = project gl, pf_env gl, sig_it gl in
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
index 8817d82..d76f761 100644
--- a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
@@ -3840,7 +3840,8 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl =
       (mkApp (compose_lam l c, Array.of_list (mkRel 1 :: mkRels n)))
   in
   pp(lazy(str"after: " ++ pr_constr oc));
-  try applyn ~with_evars ~with_shelve:true ?beta n oc gl with _ -> raise dependent_apply_error
+  try applyn ~with_evars ~with_shelve:true ?beta n oc gl
+  with e when Errors.noncritical e -> raise dependent_apply_error
 
 let pf_fresh_inductive_instance ind gl =
   let sigma, env, it = project gl, pf_env gl, sig_it gl in
-- 
cgit v1.2.3