From 63ae87d51456add79652b42b972d6be93b6119bc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 17 Dec 2016 15:50:10 +0100 Subject: Fix a mishandled exception in Omega. Due to the introduction of the monadic layer, an exception was raised at a later time and not caught properly. --- plugins/omega/coq_omega.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'plugins/omega/coq_omega.ml') diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 8c2f0f53f..72aeb9066 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1859,7 +1859,9 @@ let destructure_goal = let decidability = Tacmach.New.of_old decidability gl in let rec loop t = Proofview.tclEVARMAP >>= fun sigma -> - match destructurate_prop sigma t with + let prop () = Proofview.tclUNIT (destructurate_prop sigma t) in + Proofview.V82.wrap_exceptions prop >>= fun prop -> + match prop with | Kapp(Not,[t]) -> (Tacticals.New.tclTHEN (Tacticals.New.tclTHEN (unfold sp_not) intro) -- cgit v1.2.3