From 4e84e83911c1cf7613a35b921b1e68e097f84b5a Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:11:47 +0200
Subject: Remove unused [open] statements

---
 plugins/firstorder/instances.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 62f811546d..2b624b9833 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -17,7 +17,6 @@ open Tacmach.New
 open Tactics
 open Tacticals.New
 open Proofview.Notations
-open Termops
 open Reductionops
 open Formula
 open Sequent
-- 
cgit v1.2.3


From 87910d7be9bd50de4db80f70c6e287c7c7994460 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Tue, 25 Apr 2017 14:31:15 +0200
Subject: Fix 4.04 warnings

---
 plugins/firstorder/g_ground.ml4 | 1 -
 1 file changed, 1 deletion(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 8ef6a09d0e..b250175354 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -123,7 +123,6 @@ let normalize_evaluables=
 	   unfold_in_hyp (Lazy.force defined_connectives)
 	   (Tacexpr.InHypType id)) *)
 
-open Pp
 open Genarg
 open Ppconstr
 open Printer
-- 
cgit v1.2.3


From 9a48211ea8439a8502145e508b70ede9b5929b2f Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Thu, 27 Apr 2017 21:58:52 +0200
Subject: Post-rebase warnings (unused opens and 2 unused values)

---
 plugins/firstorder/formula.ml   | 1 -
 plugins/firstorder/instances.ml | 1 -
 plugins/firstorder/rules.ml     | 1 -
 plugins/firstorder/rules.mli    | 1 -
 plugins/firstorder/sequent.ml   | 1 -
 plugins/firstorder/sequent.mli  | 2 --
 6 files changed, 7 deletions(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index ade94e98e3..9900792cac 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -12,7 +12,6 @@ open Term
 open EConstr
 open Vars
 open Termops
-open Tacmach
 open Util
 open Declarations
 open Globnames
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 2b624b9833..5a1e7c26a1 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -10,7 +10,6 @@ open Unify
 open Rules
 open CErrors
 open Util
-open Term
 open EConstr
 open Vars
 open Tacmach.New
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index e0d2c38a73..86a6770070 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -9,7 +9,6 @@
 open CErrors
 open Util
 open Names
-open Term
 open EConstr
 open Vars
 open Tacmach.New
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index 80a7ae2c25..fb21730830 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -8,7 +8,6 @@
 
 open Term
 open EConstr
-open Tacmach
 open Names
 open Globnames
 
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 59b842c825..2d18b66054 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -12,7 +12,6 @@ open CErrors
 open Util
 open Formula
 open Unify
-open Tacmach
 open Globnames
 open Pp
 
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 18d68f54f9..6ed251f34e 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -6,10 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Term
 open EConstr
 open Formula
-open Tacmach
 open Globnames
 
 module OrderedConstr: Set.OrderedType with type t=Constr.t
-- 
cgit v1.2.3