diff options
| author | Hugo Herbelin | 2015-10-31 15:49:09 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2015-11-02 15:46:40 +0100 |
| commit | 4e643d134f02cfa9a73754c3cf48048541324834 (patch) | |
| tree | 54a8d34fb69fd23b1d5034f13c2cafb20fcc3e0f /intf | |
| parent | 69be6a29cf9f774cb4afe94d76b157ba50984c1d (diff) | |
Adding syntax "Show id" to show goal named id (shelved or not).
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.mli | 3 |
1 files changed, 2 insertions, 1 deletions
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 |