diff options
Diffstat (limited to 'tactics/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 |