5 files changed, 15 insertions, 10 deletions
diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4
index 7e58ef9a3e..565308f72e 100644
--- a/plugins/rtauto/g_rtauto.ml4
+++ b/plugins/rtauto/g_rtauto.ml4
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
+
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
 open Ltac_plugin
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 4eef1b0a75..8dd7a5e469 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open CErrors
 open Util
 open Goptions
@@ -145,7 +146,7 @@ let add_step s sub =
     | SI_Or_r,[p] -> I_Or_r p
     | SE_Or i,[p1;p2] -> E_Or(i,p1,p2)
     | SD_Or i,[p] -> D_Or(i,p)
-    | _,_ -> anomaly ~label:"add_step" (Pp.str "wrong arity")
+    | _,_ -> anomaly ~label:"add_step" (Pp.str "wrong arity.")
 
 type 'a with_deps =
     {dep_it:'a;
@@ -167,7 +168,7 @@ type state =
 
 let project = function
     Complete prf -> prf
-  | Incomplete (_,_) -> anomaly (Pp.str "not a successful state")
+  | Incomplete (_,_) -> anomaly (Pp.str "not a successful state.")
 
 let pop n prf =
   let nprf=
@@ -361,7 +362,7 @@ let search_norev seq=
 		     (Arrow(f2,f3)))
 		  f1;
 		add_hyp (embed nseq) f3]):: !goals
-      | _ -> anomaly ~label:"search_no_rev" (Pp.str "can't happen") in
+      | _ -> anomaly ~label:"search_no_rev" (Pp.str "can't happen.") in
     Int.Map.iter add_one seq.norev_hyps;
     List.rev !goals
 
@@ -386,7 +387,7 @@ let search_in_rev_hyps seq=
 	| Arrow (Disjunct (f1,f2),f0) ->
 	    [make_step (SD_Or(i)),
 	     [add_hyp (add_hyp (embed nseq) (Arrow(f1,f0))) (Arrow (f2,f0))]]
-	| _ -> anomaly ~label:"search_in_rev_hyps" (Pp.str "can't happen")
+	| _ -> anomaly ~label:"search_in_rev_hyps" (Pp.str "can't happen.")
   with
       Not_found -> search_norev seq
 
@@ -464,7 +465,7 @@ let branching = function
 	  | _::next ->
 	      s_info.nd_branching<-s_info.nd_branching+List.length next in
 	List.map (append stack) successors
-  | Complete prf -> anomaly (Pp.str "already succeeded")
+  | Complete prf -> anomaly (Pp.str "already succeeded.")
 
 open Pp
 
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 1b07a8ca84..f84eebadce 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
+
 module Search = Explore.Make(Proof_search)
 
 open Ltac_plugin
@@ -299,7 +301,7 @@ let rtauto_tac gls=
 		      build_form formula;
 		      build_proof [] 0 prf|]) in
   let term=
-    applist (main,List.rev_map (fun (id,_) -> mkVar id) hyps) in
+    applistc main (List.rev_map (fun (id,_) -> mkVar id) hyps) in
   let build_end_time=System.get_time () in
   let _ = if !verbose then
     begin
diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli
index 0925523641..ac260e51ac 100644
--- a/plugins/rtauto/refl_tauto.mli
+++ b/plugins/rtauto/refl_tauto.mli
@@ -7,16 +7,18 @@
 (************************************************************************)
 (* raises Not_found if no proof is found *)
 
+open API
+
 type atom_env=
     {mutable next:int;
      mutable env:(Term.constr*int) list}
 
 val make_form : atom_env ->
-    Proof_type.goal Tacmach.sigma -> EConstr.types -> Proof_search.form
+    Proof_type.goal Evd.sigma -> EConstr.types -> Proof_search.form
 
 val make_hyps :
     atom_env ->
-    Proof_type.goal Tacmach.sigma ->
+    Proof_type.goal Evd.sigma ->
     EConstr.types list ->
     EConstr.named_context ->
     (Names.Id.t * Proof_search.form) list
diff --git a/plugins/rtauto/vo.itarget b/plugins/rtauto/vo.itarget
deleted file mode 100644
index 4c9364ad72..0000000000
--- a/plugins/rtauto/vo.itarget
+++ /dev/null
@@ -1,2 +0,0 @@
-Bintree.vo
-Rtauto.vo