From d5fece25d8964d5d9fcd55b66164286aeef5fb9f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Aug 2014 20:44:03 +0200
Subject: Reorganization of tactics: - made "apply" tactics of type
 Proofview.tactic, as well as other inner   functions about elim and assert -
 used same hypothesis naming policy for intros and internal_cut (towards a  
 reorganization of intro patterns) - "apply ... in H as pat" now supports any
 kind of introduction   pattern (doc not changed)

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

(limited to 'plugins/omega')

diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 271cade276..48c853029e 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -37,7 +37,7 @@ let elim_id id =
   Proofview.Goal.enter begin fun gl ->
     simplest_elim (Tacmach.New.pf_global id gl)
   end
-let resolve_id id gl = apply (pf_global gl id) gl
+let resolve_id id gl = Proofview.V82.of_tactic (apply (pf_global gl id)) gl
 
 let timing timer_name f arg = f arg
 
-- 
cgit v1.2.3