diff options
| author | Enrico Tassi | 2020-06-13 21:17:32 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2020-06-15 10:59:53 +0200 |
| commit | 73c3dd110402f182229d8a21458758424256d64c (patch) | |
| tree | 883354b9112c8096595abf62a0cdd9f11f48f7cc /plugins/ssr | |
| parent | 13e8d04b2f080fbc7ca169bc39e53c8dd091d279 (diff) | |
[ssr] remove catch all
Diffstat (limited to 'plugins/ssr')
| -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) -> |