aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder/instances.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder/instances.ml')
-rw-r--r--plugins/firstorder/instances.ml4
1 files changed, 0 insertions, 4 deletions
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index ee1c44265..e3367b4c2 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -6,11 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Formula
-open Sequent
open Unify
open Rules
-open Pp
open Errors
open Util
open Term
@@ -20,7 +17,6 @@ open Tactics
open Tacticals
open Termops
open Reductionops
-open Declarations
open Formula
open Sequent
open Names