From d5f3727e0c218be41f0c5547677761fa7223e744 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 25 Apr 2014 18:33:27 +0200 Subject: Removing useless try-with clauses in Goal.enter variants. --- plugins/omega/coq_omega.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'plugins/omega/coq_omega.ml') diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index de20756b3..9b851447c 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1825,9 +1825,7 @@ let destructure_hyps = end in let hyps = Proofview.Goal.hyps gl in - try (* type_of can raise exceptions *) - loop hyps - with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + loop hyps end let destructure_goal = -- cgit v1.2.3