From 15effb7dedbaa407bbe25055da6efded366dd3b1 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Sat, 2 Nov 2013 15:35:31 +0000
Subject: 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
---
 plugins/omega/coq_omega.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'plugins/omega')

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 ->
-- 
cgit v1.2.3