From e56cfa2d9eeedbcbf6ce865380d9ee42c014f77e Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 4 Jan 2022 13:53:38 +0100
Subject: [PATCH] [wp] Print goal id and short id in proof script
---
src/plugins/wp/GuiGoal.ml | 2 ++
1 file changed, 2 insertions(+)
diff --git a/src/plugins/wp/GuiGoal.ml b/src/plugins/wp/GuiGoal.ml
index 6fb5dd22d7e..5f3a55b090e 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 ()
--
GitLab