diff options
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 13 |
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 |