diff options
| -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 |