[ssr] wrap a couple of exception with tclLIFT

1 files changed, 8 insertions, 5 deletions

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 06b26b28fd..e05c4c26dd 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1500,14 +1500,17 @@ end
 let tacMK_SSR_CONST name =
   Proofview.tclENV >>= fun env ->
   Proofview.tclEVARMAP >>= fun sigma ->
-  let sigma, c = mkSsrConst name env sigma in
-  Unsafe.tclEVARS sigma <*>
-  tclUNIT c
+  match mkSsrConst name env sigma with
+  | sigma, c -> Unsafe.tclEVARS sigma <*> tclUNIT c
+  | exception e when CErrors.noncritical e ->
+    tclLIFT (Proofview.NonLogical.raise (e, Exninfo.null))
 
 let tacDEST_CONST c =
   Proofview.tclEVARMAP >>= fun sigma ->
-  let c, _ = EConstr.destConst sigma c in
-  tclUNIT c
+  match EConstr.destConst sigma c with
+  | c, _ -> tclUNIT c
+  | exception e when CErrors.noncritical e ->
+    tclLIFT (Proofview.NonLogical.raise (e, Exninfo.null))
 
 (* TASSI: This version of unprotects inlines the unfold tactic definition,
  * since we don't want to wipe out let-ins, and it seems there is no flag