diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_proofs.ml4 | 4 |
1 files changed, 3 insertions, 1 deletions
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 |