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/vernacexpr.ml | |
| parent | 767898e6e59e86e3123846374448402360b783e6 (diff) | |
[vernac] Add a “deprecated” attribute
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 f5f37339c..57ccb6006 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -463,6 +463,7 @@ type nonrec vernac_flag = | VernacProgram | VernacPolymorphic of bool | VernacLocal of bool + | VernacDeprecated of string * string (* Since, Note *) type vernac_control = | VernacExpr of vernac_flag list * vernac_expr |