diff options
Diffstat (limited to 'plugins/omega')
| -rw-r--r-- | plugins/omega/coq_omega.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 70c6d22121..865fb386a8 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1782,7 +1782,9 @@ let destructure_hyps = end in Proofview.Goal.hyps >>= fun hyps -> - loop (Environ.named_context_of_val hyps) + try (* type_of can raise exceptions *) + loop (Environ.named_context_of_val hyps) + with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e let destructure_goal = Proofview.Goal.concl >>= fun concl -> |