aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder/g_ground.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder/g_ground.ml4')
-rw-r--r--plugins/firstorder/g_ground.ml41
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index b04c4a50c..134b6ba94 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -18,7 +18,6 @@ open Libnames
open Constrarg
open Stdarg
open Pcoq.Prim
-open Pcoq.Tactic
DECLARE PLUGIN "ground_plugin"