diff options
-rw-r--r-- | vernac/ppvernac.ml | 24 | ||||
-rw-r--r-- | vernac/vernacentries.ml | 4 | ||||
-rw-r--r-- | vernac/vernacexpr.ml | 1 | ||||
-rw-r--r-- | vernac/vernacinterp.ml | 5 | ||||
-rw-r--r-- | vernac/vernacinterp.mli | 3 |
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 |