3 files changed, 8 insertions, 5 deletions
diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4
index d27b04834e..7e58ef9a3e 100644
--- a/plugins/rtauto/g_rtauto.ml4
+++ b/plugins/rtauto/g_rtauto.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
+open Ltac_plugin
+
 DECLARE PLUGIN "rtauto_plugin"
 
 TACTIC EXTEND rtauto
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 8b92611136..1ad4d622b2 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -505,12 +505,12 @@ let pp_mapint map =
 		pp_form obj ++ str " => " ++
 				 pp_list (fun (i,f) -> pp_form f) l ++
 				 cut ()) ) map;
-    str "{ " ++ vb 0 ++  (!pp) ++ str " }" ++ close ()
+    str "{ " ++ hv 0 (!pp ++ str " }")
 
 let pp_connect (i,j,f1,f2) = pp_form f1 ++ str " => " ++ pp_form f2
 
 let pp_gl gl= cut () ++
-  str "{ " ++ vb 0 ++
+  str "{ " ++ hv 0 (
 	      begin
 		match gl.abs with
 		    None -> str ""
@@ -520,7 +520,7 @@ let pp_gl gl= cut () ++
   str "norev =" ++ pp_intmap gl.norev_hyps ++ cut () ++
   str "arrows=" ++ pp_mapint gl.right ++ cut () ++
   str "cnx   =" ++ pp_list pp_connect gl.cnx ++ cut () ++
-  str "goal  =" ++ pp_form gl.gl ++ str " }" ++ close ()
+  str "goal  =" ++ pp_form gl.gl ++ str " }")
 
 let pp =
   function
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 4ed9079517..35d6768c13 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -8,6 +8,7 @@
 
 module Search = Explore.Make(Proof_search)
 
+open Ltac_plugin
 open CErrors
 open Util
 open Term
@@ -263,7 +264,7 @@ let rtauto_tac gls=
   let _=
     if Retyping.get_sort_family_of
       (pf_env gls) (Tacmach.project gls) gl != InProp
-    then errorlabstrm "rtauto" (Pp.str "goal should be in Prop") in
+    then user_err ~hdr:"rtauto" (Pp.str "goal should be in Prop") in
   let glf=make_form gamma gls gl in
   let hyps=make_hyps gamma gls [gl] (pf_hyps gls) in
   let formula=
@@ -282,7 +283,7 @@ let rtauto_tac gls=
   let prf =
     try project (search_fun (init_state [] formula))
     with Not_found ->
-      errorlabstrm "rtauto" (Pp.str "rtauto couldn't find any proof") in
+      user_err ~hdr:"rtauto" (Pp.str "rtauto couldn't find any proof") in
   let search_end_time = System.get_time () in
   let _ = if !verbose then
     begin