diff --git a/dev/include_printers b/dev/include_printers
index 480f8887d665..1aa0e1c10d53 100644
--- a/dev/include_printers
+++ b/dev/include_printers
@@ -34,6 +34,7 @@
 (*#install_printer  (* hint_db *)  print_hint_db;;*)
 (*#install_printer  (* hints_path *)  pphintspath;;*)
 #install_printer  (* goal *)  ppgoal;;
+#install_printer  ppgoal_with_state;;
 (*#install_printer  (* sigma goal *)  ppsigmagoal;;*)
 #install_printer  (* proof *)  pproof;;
 #install_printer  (* proofview *)  ppproofview;;
diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg
index 381ab01a0a0a..c2762891a324 100644
--- a/dev/top_printers.dbg
+++ b/dev/top_printers.dbg
@@ -61,6 +61,7 @@ install_printer Top_printers.ppexistentialset
 install_printer Top_printers.ppexistentialfilter
 install_printer Top_printers.ppclenv
 install_printer Top_printers.ppgoal
+install_printer Top_printers.ppgoal_with_state
 install_printer Top_printers.pphintdb
 install_printer Top_printers.ppproofview
 install_printer Top_printers.ppopenconstr
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 05b75b6fe88a..dbdeec44ba9e 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -230,6 +230,7 @@ let ppexistentialfilter filter = match Evd.Filter.repr filter with
 let pr_goal e = Pp.(str "GOAL:" ++ int (Evar.repr e))
 let ppclenv clenv = pp(pr_clenv clenv)
 let ppgoal g = pp(Printer.Debug.pr_goal g)
+let ppgoal_with_state g = ppevar (Proofview_monad.drop_state g)
 let pphintdb db = pp(envpp Hints.pr_hint_db_env db)
 let ppproofview p =
   let gls,sigma = Proofview.proofview p in
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index 3e81d47c3fd6..cac4ac13d3d0 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -134,6 +134,7 @@ val ppexistentialfilter : Evd.Filter.t -> unit
 val ppclenv : Clenv.clausenv -> unit
 
 val ppgoal : Proofview.Goal.t -> unit
+val ppgoal_with_state : Proofview_monad.goal_with_state -> unit
 
 val pphintdb : Hints.Hint_db.t -> unit
 val ppproofview : Proofview.proofview -> unit