7 files changed, 9 insertions, 2 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index d67dceeac6..566b2b8b08 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -12,6 +12,7 @@ open Term
 open Termops
 open Reductionops
 open Tacmach
+open Errors
 open Util
 open Declarations
 open Libnames
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 4a38c48dcf..f5b16e43fe 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -17,7 +17,6 @@ open Tacticals
 open Tacinterp
 open Term
 open Names
-open Util
 open Libnames
 
 (* declaring search depth as a global option *)
@@ -103,6 +102,7 @@ let normalize_evaluables=
 	   unfold_in_hyp (Lazy.force defined_connectives)
 	   (Tacexpr.InHypType id)) *)
 
+open Pp
 open Genarg
 open Ppconstr
 open Printer
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 16831d3ecc..8d4b0eee1c 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -10,6 +10,8 @@ open Formula
 open Sequent
 open Unify
 open Rules
+open Pp
+open Errors
 open Util
 open Term
 open Glob_term
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 23eeb2f662..b56fe4e509 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Term
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index f75678c60f..780e3f3e7e 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Term
+open Errors
 open Util
 open Formula
 open Unify
@@ -235,7 +236,7 @@ let print_cmap map=
   let print_entry c l s=
     let xc=Constrextern.extern_constr false (Global.env ()) c in
       str "| " ++
-      Util.prlist Printer.pr_global l ++
+      prlist Printer.pr_global l ++
       str " : " ++
       Ppconstr.pr_constr_expr xc ++
       cut () ++
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index c5c2bb9541..5587e9fbb5 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Term
+open Errors
 open Util
 open Formula
 open Tacmach
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 299a0054a2..48c402cc0f 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Formula
 open Tacmach