diff --git a/src/plugins/wp/GuiGoal.ml b/src/plugins/wp/GuiGoal.ml
index 6fb5dd22d7e1c924a220c2556714929b4de685e4..5f3a55b090e876ed2c3454b29e6fdce536e4ce80 100644
--- a/src/plugins/wp/GuiGoal.ml
+++ b/src/plugins/wp/GuiGoal.ml
@@ -558,6 +558,8 @@ class pane (gprovers : GuiConfig.provers) =
               scripter#tree proof ;
               text#hrule ;
               text#printf "%t@." (printer#goal (ProofEngine.head proof)) ;
+              text#printf "@{<bf>Goal id:@}  %s@." main.po_gid ;
+              text#printf "@{<bf>Short id:@} %s@." main.po_sid ;
               text#hrule ;
               scripter#status proof ;
             end ()