diff --git a/src/abstraction.mlg b/src/abstraction.mlg
index 8a8c9f2..989d604 100644
--- a/src/abstraction.mlg
+++ b/src/abstraction.mlg
@@ -15,20 +15,18 @@
 DECLARE PLUGIN "coq-paramcoq.plugin"
 
 {
-open Ltac_plugin
 open Feedback
 open Stdarg
-open Tacarg
 open Parametricity
 open Declare_translation
 }
 
 VERNAC COMMAND EXTEND SetParametricityTactic CLASSIFIED AS SIDEFF
 | #[ locality = Tactic_option.tac_option_locality; ]
-  [ "Parametricity" "Tactic" ":=" tactic(t) ] -> {
+  [ "Parametricity" "Tactic" ":=" generic_tactic(t) ] -> {
     Relations.set_parametricity_tactic
       locality
-      (Tacintern.glob_tactic t) }
+      (Gentactic.intern (Global.env()) t) }
 END
 
 VERNAC COMMAND EXTEND ShowTable CLASSIFIED AS QUERY
diff --git a/src/dune b/src/dune
index 3c06cd2..d02b4ea 100644
--- a/src/dune
+++ b/src/dune
@@ -3,6 +3,6 @@
  (public_name coq-paramcoq.plugin)
  (synopsis "Plugin for generating parametricity statements to perform refinement proofs")
  (flags :standard -rectypes -w -9-27)
- (libraries coq-core.plugins.ltac))
+ (libraries coq-core.plugins.ltac)) ; not sure if ltac dep is real
 
 (coq.pp (modules abstraction))
diff --git a/src/relations.ml b/src/relations.ml
index 44a1d06..4bd11d9 100644
--- a/src/relations.ml
+++ b/src/relations.ml
@@ -10,7 +10,6 @@
 (**************************************************************************)
 
 
-open Ltac_plugin
 open Names
 open Globnames
 open Libobject