From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 plugins/romega/g_romega.ml4 | 18 +++++++++++++-----
 1 file changed, 13 insertions(+), 5 deletions(-)

(limited to 'plugins/romega/g_romega.ml4')

diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 0a99a26b..830dc54d 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -10,16 +10,24 @@
 
 DECLARE PLUGIN "romega_plugin"
 
+open Names
 open Refl_omega
+open Constrarg
+
+let eval_tactic name =
+  let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in
+  let kn = KerName.make2 (MPfile dp) (Label.make name) in
+  let tac = Tacenv.interp_ltac kn in
+  Tacinterp.eval_tactic tac
 
 let romega_tactic l =
   let tacs = List.map
     (function
-       | "nat" -> Tacinterp.interp <:tactic<zify_nat>>
-       | "positive" -> Tacinterp.interp <:tactic<zify_positive>>
-       | "N" -> Tacinterp.interp <:tactic<zify_N>>
-       | "Z" -> Tacinterp.interp <:tactic<zify_op>>
-       | s -> Errors.error ("No ROmega knowledge base for type "^s))
+       | "nat" -> eval_tactic "zify_nat"
+       | "positive" -> eval_tactic "zify_positive"
+       | "N" -> eval_tactic "zify_N"
+       | "Z" -> eval_tactic "zify_op"
+       | s -> CErrors.error ("No ROmega knowledge base for type "^s))
     (Util.List.sort_uniquize String.compare l)
   in
   Tacticals.New.tclTHEN
-- 
cgit v1.2.3