[vernac] Add a “deprecated” attribute

5 files changed, 27 insertions, 10 deletions

diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index b49fb011b..f9237c775 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1193,14 +1193,24 @@ open Pputils
       | VernacEndSubproof ->
         return (str "}")
 
+let rec pr_vernac_flag_data (k, v) =
+  let k = keyword k in
+  match v with
+  | `Empty -> k
+  | `Leaf v -> k ++ str " = " ++ qs v
+  | `Node m -> k ++ str "( " ++ prlist_with_sep (fun () -> str ", ") pr_vernac_flag_data m ++ str " )"
+
 let pr_vernac_flag f =
-  keyword (match f with
-  | VernacPolymorphic true -> "polymorphic"
-  | VernacPolymorphic false -> "monomorphic"
-  | VernacProgram -> "program"
-  | VernacLocal true -> "local"
-  | VernacLocal false -> "global"
-  )
+  match f with
+  | VernacPolymorphic true -> keyword "polymorphic"
+  | VernacPolymorphic false -> keyword "monomorphic"
+  | VernacProgram -> keyword "program"
+  | VernacLocal true -> keyword "local"
+  | VernacLocal false -> keyword "global"
+  | VernacDeprecated (since, note) ->
+    pr_vernac_flag_data ("deprecated", `Node [
+        "since", `Leaf since; "note", `Leaf note
+      ])
 
 let pr_vernac_flag_list =
   function
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
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
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 36b8a7e62..30c1ddbfd 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -19,10 +19,11 @@ type atts = {
   locality : bool option;
   polymorphic : bool;
   program : bool;
+  deprecated : (string * string) option;
 }
 
-let mk_atts ?(loc=None) ?(locality=None) ?(polymorphic=false) ?(program=false) () : atts =
-  { loc ; locality ; polymorphic ; program }
+let mk_atts ?(loc=None) ?(locality=None) ?(polymorphic=false) ?(program=false) ?(deprecated=None) () : atts =
+  { loc ; locality ; polymorphic ; program ; deprecated }
 
 type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
 
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index a24bcd40d..362c05d4c 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -17,10 +17,11 @@ type atts = {
   locality : bool option;
   polymorphic : bool;
   program : bool;
+  deprecated : (string * string) option; (* Since, Note *)
 }
 
 val mk_atts : ?loc: Loc.t option -> ?locality: bool option ->
-  ?polymorphic: bool -> ?program: bool -> unit -> atts
+  ?polymorphic: bool -> ?program: bool -> ?deprecated: (string * string) option -> unit -> atts
 
 type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t