From 699b70cd9ad0d79cbde228bdb51fde224a3b524e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 14 Sep 2016 17:19:14 +0200 Subject: Moving Ltac-specific parsing API to ltac/ folder. --- plugins/setoid_ring/g_newring.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/setoid_ring') 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" -- cgit v1.2.3