Adding syntax "Show id" to show goal named id (shelved or not).

7 files changed, 27 insertions, 10 deletions

diff --git a/CHANGES b/CHANGES
index cf0f4446f4..019c6cdb24 100644
--- a/CHANGES
+++ b/CHANGES
@@ -8,6 +8,7 @@ Vernacular commands
 - New option "Strict Universe Declaration", set by default. It enforces the
   declaration of all polymorphic universes appearing in a definition when
   introducing it.
+- New command "Show id" to show goal named id.
 
 Tactics
 
@@ -36,7 +37,6 @@ Tactics
 - Hints costs are now correctly taken into account (potential source of
   incompatibilities).
 
-
 API
 
 - Some functions from pretyping/typing.ml and their derivatives were potential
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index f89f076b5f..99264dbe0a 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -40,7 +40,8 @@ type scope_name = string
 type goal_reference =
   | OpenSubgoals
   | NthGoal of int
-  | GoalId of goal_identifier
+  | GoalId of Id.t
+  | GoalUid of goal_identifier
 
 type printable =
   | PrintTables
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 7f5459bfa6..017f0ea50b 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -73,8 +73,10 @@ GEXTEND Gram
       | IDENT "Unfocused" -> VernacUnfocused
       | IDENT "Show" -> VernacShow (ShowGoal OpenSubgoals)
       | IDENT "Show"; n = natural -> VernacShow (ShowGoal (NthGoal n))
+      | IDENT "Show"; id = ident -> VernacShow (ShowGoal (GoalId id))
+      | IDENT "Show"; IDENT "Goal" -> VernacShow (ShowGoal (GoalId (Names.Id.of_string "Goal")))
       | IDENT "Show"; IDENT "Goal"; n = string ->
-          VernacShow (ShowGoal (GoalId n))
+          VernacShow (ShowGoal (GoalUid n))
       | IDENT "Show"; IDENT "Implicit"; IDENT "Arguments"; n = OPT natural ->
 	  VernacShow (ShowGoalImplicitly n)
       | IDENT "Show"; IDENT "Node" -> VernacShow ShowNode
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 00c276bdbe..72b9cafe3f 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -594,7 +594,8 @@ module Make
           let pr_goal_reference = function
             | OpenSubgoals -> mt ()
             | NthGoal n -> spc () ++ int n
-            | GoalId n -> spc () ++ str n in
+            | GoalId id -> spc () ++ pr_id id
+            | GoalUid n -> spc () ++ str n in
           let pr_showable = function
             | ShowGoal n -> keyword "Show" ++ pr_goal_reference n
             | ShowGoalImplicitly n -> keyword "Show Implicit Arguments" ++ pr_opt int n
diff --git a/printing/printer.ml b/printing/printer.ml
index 202b4f2bc7..2e112f9ace 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -455,14 +455,17 @@ let pr_ne_evar_set hd tl sigma l =
   else
     mt ()
 
+let pr_selected_subgoal name sigma g =
+  let pg = default_pr_goal { sigma=sigma ; it=g; } in
+  v 0 (str "subgoal " ++ name ++ pr_goal_tag g ++ pr_goal_name sigma g
+       ++ str " is:" ++ cut () ++ pg)
+
 let default_pr_subgoal n sigma =
   let rec prrec p = function
     | [] -> error "No such goal."
     | g::rest ->
 	if Int.equal p 1 then
-          let pg = default_pr_goal { sigma=sigma ; it=g; } in
-          v 0 (str "subgoal " ++ int n ++ pr_goal_tag g ++ pr_goal_name sigma g 
-	       ++ str " is:" ++ cut () ++ pg)
+          pr_selected_subgoal (int n) sigma g
 	else
 	  prrec (p-1) rest
   in
@@ -652,9 +655,17 @@ let pr_nth_open_subgoal n =
 
 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 ->
+      let g = Evd.evar_key id sigma in
+      pr_selected_subgoal (pr_id id) sigma g)
+  with Not_found -> error "No such goal."
+
+let pr_goal_by_uid uid =
+  let p = Proof_global.give_me_the_proof () in
+  let g = Goal.get_by_uid uid in
   let pr gs =
-    v 0 (str "goal / evar " ++ str id ++ str " is:" ++ cut ()
+    v 0 (str "goal / evar " ++ str uid ++ str " is:" ++ cut ()
 	 ++ pr_goal gs)
   in
   try
diff --git a/printing/printer.mli b/printing/printer.mli
index 0a44e4f103..5c60b89366 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -176,7 +176,8 @@ module ContextObjectMap : CMap.ExtS
 val pr_assumptionset :
   env -> Term.types ContextObjectMap.t -> std_ppcmds
 
-val pr_goal_by_id : string -> std_ppcmds
+val pr_goal_by_id : Id.t -> std_ppcmds
+val pr_goal_by_uid : string -> std_ppcmds
 
 type printer_pr = {
  pr_subgoals            : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds;
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 31bfc004a8..b6a1a53fa8 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1786,6 +1786,7 @@ let vernac_show = function
       | OpenSubgoals -> pr_open_subgoals ()
       | NthGoal n -> pr_nth_open_subgoal n
       | GoalId id -> pr_goal_by_id id
+      | GoalUid id -> pr_goal_by_uid id
     in
     msg_notice info
   | ShowGoalImplicitly None ->