From 636af8ab15807a93ce08778fac18cbe273fcf49d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 1 Aug 2014 01:13:42 +0200
Subject: Removing some tactic compatibility layer.

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

(limited to 'plugins')

diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 83f3462428..271cade276 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1850,7 +1850,7 @@ let destructure_goal =
                 (Proofview.V82.tactic (Tactics.refine
 		                         (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |]))))
 	        intro
-	    with Undecidable -> Proofview.V82.tactic (Tactics.elim_type (build_coq_False ()))
+	    with Undecidable -> Tactics.elim_type (build_coq_False ())
 	  in
 	  Tacticals.New.tclTHEN goal_tac destructure_hyps
     in
-- 
cgit v1.2.3