diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:35:31 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:35:31 +0000 |
| commit | 15effb7dedbaa407bbe25055da6efded366dd3b1 (patch) | |
| tree | 70a229b9e69d16f6fab4afdd3d15957de23b0dc1 /plugins/omega/coq_omega.ml | |
| parent | 5ac88949f0fbab1f47781c9de4edbcffa19d9896 (diff) | |
Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).
They were a hack to avoid looking where exceptions were raised and not
caught. Hopefully I produce a cleaner stack now, catching errors when
it is needed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16980 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/omega/coq_omega.ml')
| -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 70c6d2212..865fb386a 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 -> |