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 /tactics/hints.ml | |
| parent | 357f0b36bf352b26aeb5ca5c413c7bd03f615513 (diff) | |
Replacing catchable_exception by noncritical in try-with blocks.
Diffstat (limited to 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 731792e34e..9d9616354b 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -923,7 +923,7 @@ let make_resolve_hyp env sigma decl = (c, NamedDecl.get_type decl, Univ.ContextSet.empty)] with | Failure _ -> [] - | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp.") + | e when noncritical e -> anomaly (Pp.str "make_resolve_hyp.") (* REM : in most cases hintname = id *) |