diff options
| author | Hugo Herbelin | 2020-03-02 23:51:54 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-13 07:37:25 +0100 |
| commit | 812665445fd370842a1b8abf7cddbd33f3ddaa5c (patch) | |
| tree | dd9659a8a81b7d56227ee4f2a2e92fbef3b27ae7 | |
| parent | bc77fdc4330c8572111102d61fd65f032b1cf5b6 (diff) | |
Fixing a non-protected try-with in class_tactics.ml.
| -rw-r--r-- | tactics/class_tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index f92d0603ca..71a2ca3752 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -189,7 +189,7 @@ let clenv_unique_resolver_tac with_evars ~flags clenv' = Proofview.Goal.enter begin fun gls -> let resolve = try Proofview.tclUNIT (clenv_unique_resolver ~flags clenv' gls) - with e -> Proofview.tclZERO e + with e when noncritical e -> Proofview.tclZERO e in resolve >>= fun clenv' -> Clenvtac.clenv_refine ~with_evars ~with_classes:false clenv' end |