diff options
Diffstat (limited to 'vernac/vernacexpr.ml')
| -rw-r--r-- | vernac/vernacexpr.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 0968632c2d..c15baf6157 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -24,6 +24,7 @@ type goal_reference = | GoalId of Id.t type printable = + | PrintTypingFlags | PrintTables | PrintFullContext | PrintSectionContext of qualid |