aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder/ground.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder/ground.ml')
-rw-r--r--plugins/firstorder/ground.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 58bef84ea..753fdda72 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -12,9 +12,7 @@ open Rules
open Instances
open Term
open Tacmach
-open Tactics
open Tacticals
-open Libnames
let update_flags ()=
let predref=ref Names.Cpred.empty in