aboutsummaryrefslogtreecommitdiff
path: root/intf
diff options
context:
space:
mode:
Diffstat (limited to 'intf')
-rw-r--r--intf/vernacexpr.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index ea412a7d6a..9aef4b1312 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -39,7 +39,6 @@ type goal_reference =
| OpenSubgoals
| NthGoal of int
| GoalId of Id.t
- | GoalUid of goal_identifier
type printable =
| PrintTables