aboutsummaryrefslogtreecommitdiff
path: root/plugins/firstorder
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder')
-rw-r--r--plugins/firstorder/ground.ml1
-rw-r--r--plugins/firstorder/instances.mli3
-rw-r--r--plugins/firstorder/sequent.mli1
3 files changed, 0 insertions, 5 deletions
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 5133801ee7..6c1709140b 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -11,7 +11,6 @@ open Sequent
open Rules
open Instances
open Term
-open Vars
open Tacmach
open Tacticals
diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli
index 753f2d76e1..66c42e1e64 100644
--- a/plugins/firstorder/instances.mli
+++ b/plugins/firstorder/instances.mli
@@ -6,9 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Term
-open Tacmach
-open Names
open Globnames
open Rules
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 0e5223d6bd..536ee7cc34 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -9,7 +9,6 @@
open Term
open Formula
open Tacmach
-open Names
open Globnames
module OrderedConstr: Set.OrderedType with type t=constr