diff options
| author | Enrico Tassi | 2016-02-22 17:35:34 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2016-02-22 17:35:34 +0100 |
| commit | ef79db4628963c46ae66fe25f3e2aeea6db8c2e7 (patch) | |
| tree | 2731d4d68277524946cfb0dc7d1547a6555e9abb /mathcomp/ssreflect/plugin | |
| parent | 28a6d6e38df4211cd386a29c2e6e30a6426ade59 (diff) | |
Guard "catch all" exception handler using Errors.noncritical
Diffstat (limited to 'mathcomp/ssreflect/plugin')
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 3 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 | 3 |
2 files changed, 4 insertions, 2 deletions
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 |