diff --git a/src/plugins/wp/GuiGoal.ml b/src/plugins/wp/GuiGoal.ml
index f4ddd156c273631c73bb02b8cd47e8c5bce39ea7..77dbf180519ae5cf11a2dbe30e863053121cec0b 100644
--- a/src/plugins/wp/GuiGoal.ml
+++ b/src/plugins/wp/GuiGoal.ml
@@ -546,6 +546,11 @@ class pane (gprovers : GuiConfig.provers) =
           on_proof_context proof
             begin fun () ->
               text#clear ;
+              let main = ProofEngine.main proof in
+              if ProofSession.exists main then begin
+                text#printf "%a@." ProofSession.pp_script_for main ;
+                text#hrule ;
+              end ;
               scripter#tree proof ;
               text#hrule ;
               text#printf "%t@." (printer#goal (ProofEngine.head proof)) ;