diff options
| author | Hugo Herbelin | 2020-03-02 21:13:41 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-13 07:37:25 +0100 |
| commit | cd4253ee5db24873ea131554c80650ed6d5dbd13 (patch) | |
| tree | 6702b8031bfde8b9f23f6b99853e3d95b60f5275 /vernac | |
| parent | 357f0b36bf352b26aeb5ca5c413c7bd03f615513 (diff) | |
Replacing catchable_exception by noncritical in try-with blocks.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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.") |