diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index bc167d94a3..f66b1c1249 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -323,6 +323,7 @@ type vernac_expr = class_rawexpr * class_rawexpr | VernacIdentityCoercion of obsolete_locality * lident * class_rawexpr * class_rawexpr + | VernacNameSectionHypSet of lident * section_subset_descr (* Type classes *) | VernacInstance of |