From cd4253ee5db24873ea131554c80650ed6d5dbd13 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 2 Mar 2020 21:13:41 +0100
Subject: Replacing catchable_exception by noncritical in try-with blocks.

---
 vernac/vernacentries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 953faf6fdb..f2f3660520 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -484,7 +484,7 @@ let program_inference_hook env sigma ev =
     let c, _, ctx =
       Pfedit.build_by_tactic ~poly:false env (Evd.evar_universe_context sigma) concl tac
     in Evd.set_universe_context sigma ctx, EConstr.of_constr c
-  with Logic_monad.TacticFailure e when Logic.catchable_exception e ->
+  with Logic_monad.TacticFailure e when noncritical e ->
     user_err Pp.(str "The statement obligations could not be resolved \
                       automatically, write a statement definition first.")
 
-- 
cgit v1.2.3