diff options
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 1740c5a80..af0f19834 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2335,6 +2335,10 @@ let attributes_of_flags f atts = (polymorphism, { atts with locality = Some b }) | VernacLocal _ -> user_err Pp.(str "Locality specified twice") + | VernacDeprecated (since, note) when Option.is_empty atts.deprecated -> + (polymorphism, { atts with deprecated = Some (since, note) }) + | VernacDeprecated _ -> + user_err Pp.(str "Deprecation specified twice") ) (None, atts) f |