Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the uid returned by Goal.uid.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14467 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 0 deletions

diff --git a/parsing/printer.ml b/parsing/printer.ml
index 046d55ae3c..232551984b 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -403,6 +403,13 @@ let pr_nth_open_subgoal n =
   let { it=gls ; sigma=sigma } = Proof.V82.subgoals pf in
   pr_subgoal n sigma gls
 
+let pr_goal_by_id id =
+  let p = Proof_global.give_me_the_proof () in
+  let g = Goal.get_by_uid id in
+  try
+    Proof.in_proof p (fun sigma -> pr_goal {it=g;sigma=sigma})
+  with Not_found -> error "Invalid goal identifier."
+
 (* Elementary tactics *)
 
 let pr_prim_rule = function