From 2ba1351849550c50e0fe2c7fc7f63758c10fb14a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Fri, 7 Apr 2017 16:31:25 +0200
Subject: Fix an unhandled exception in Omega.

---
 plugins/omega/coq_omega.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins/omega')

diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index a2016cb03..7780de712 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1884,6 +1884,7 @@ let destructure_goal =
 		                         (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |]))))
 	        intro
 	    with Undecidable -> Tactics.elim_type (Lazy.force coq_False)
+	    | e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
 	  in
 	  Tacticals.New.tclTHEN goal_tac destructure_hyps
     in
-- 
cgit v1.2.3