From 73c3dd110402f182229d8a21458758424256d64c Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sat, 13 Jun 2020 21:17:32 +0200
Subject: [ssr] remove catch all

---
 plugins/ssr/ssrequality.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

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) ->
-- 
cgit v1.2.3