diff options
| author |  Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-06-25 08:00:47 +0000 |
|---|---|---|
| committer | Vincent Laporte <Vincent.Laporte@gmail.com> | 2018-07-03 15:59:33 +0000 |
| commit | 5494c46f6219bea902fcc5ed983e16d1105fec51 (patch) | |
| tree | b3203230412cad19f08cb7b549074d8fea523844 /vernac/vernacentries.ml | |
| parent | 767898e6e59e86e3123846374448402360b783e6 (diff) | |
[vernac] Add a “deprecated” attribute
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 |