5 files changed, 2 insertions, 6 deletions
diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4
index 69a2043f64..bfa1e5f393 100644
--- a/plugins/rtauto/g_rtauto.ml4
+++ b/plugins/rtauto/g_rtauto.ml4
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 1158817d62..43a4107add 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 open CErrors
 open Util
 open Goptions
diff --git a/plugins/rtauto/proof_search.mli b/plugins/rtauto/proof_search.mli
index e0c09f394c..86231cf199 100644
--- a/plugins/rtauto/proof_search.mli
+++ b/plugins/rtauto/proof_search.mli
@@ -38,9 +38,9 @@ val branching: state -> state list
 
 val success: state -> bool
 
-val pp: state -> Pp.std_ppcmds
+val pp: state -> Pp.t
 
-val pr_form : form -> Pp.std_ppcmds
+val pr_form : form -> Pp.t
 
 val reset_info : unit -> unit
 
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 944e0ac5e7..9f02388c39 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 
 module Search = Explore.Make(Proof_search)
 
diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli
index 080dcdac27..bec18f6df8 100644
--- a/plugins/rtauto/refl_tauto.mli
+++ b/plugins/rtauto/refl_tauto.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 (* raises Not_found if no proof is found *)
 
-open API
 
 type atom_env=
     {mutable next:int;