aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/setoid_ring')
-rw-r--r--plugins/setoid_ring/g_newring.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index 216eb8b373..1a00200318 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -17,7 +17,7 @@ open Newring
open Stdarg
open Constrarg
open Pcoq.Constr
-open Pcoq.Tactic
+open Pltac
DECLARE PLUGIN "newring_plugin"