From 64ce136a5fb2eb1d3b620889b2047fda82694849 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 5 May 2020 10:21:21 +0200
Subject: [ssr] wrap a couple of exception with tclLIFT

---
 plugins/ssr/ssrcommon.ml | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

(limited to 'plugins')

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