diff options
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 29a9c65561..e25fc1100d 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -389,7 +389,7 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_ ppdebug(lazy Pp.(str"pirrel_rewrite of type: " ++ pr_econstr_env env sigma proof_ty)); try Proofview.V82.of_tactic (refine_with ~first_goes_last:(not !ssroldreworder || under) ~with_evars:under (sigma, proof)) gl - with _ -> + with e when CErrors.noncritical e -> (* we generate a msg like: "Unable to find an instance for the variable" *) let hd_ty, miss = match EConstr.kind sigma c with | App (hd, args) -> |