Module `Attributes`

type vernac_flag_type = | FlagIdent of string | FlagString of string: The type of parsing attribute data

type vernac_flags = vernac_flag list
and vernac_flag = (string * vernac_flag_value) CAst.t
and vernac_flag_value = | VernacFlagEmpty | VernacFlagLeaf of vernac_flag_type | VernacFlagList of vernac_flags

type +'a attribute: The type of attributes. When parsing attributes if an 'a attribute is present then an 'a value will be produced. In the most general case, an attribute transforms the raw flags along with its value.

val parse : 'a attribute -> vernac_flags -> 'a: Errors on unsupported attributes.

val unsupported_attributes : vernac_flags -> unit: Errors if the list of flags is nonempty.

module Notations : sig ... end

val raw_attributes : vernac_flags attribute
val polymorphic : bool attribute
val program : bool attribute
val template : bool option attribute
val locality : bool option attribute
val option_locality : Goptions.option_locality attribute
val deprecation : Deprecation.t option attribute
val canonical_field : bool attribute
val canonical_instance : bool attribute
val using : string option attribute
val hint_locality : default:(unit -> Hints.hint_locality) -> Hints.hint_locality attribute
val really_hint_locality : Hints.hint_locality attribute: With the warning for Hint (and not for Instance etc)

val typing_flags : Declarations.typing_flags option attribute: Enable/Disable universe checking

val program_mode_option_name : string list: For internal use when messing with the global option.

val only_locality : vernac_flags -> bool option: Parse attributes allowing only locality.

val only_polymorphism : vernac_flags -> bool: Parse attributes allowing only polymorphism. Uses the global flag for the default value.

val parse_drop_extra : 'a attribute -> vernac_flags -> 'a: Ignores unsupported attributes.

val parse_with_extra : 'a attribute -> vernac_flags -> vernac_flags * 'a: Returns unsupported attributes.

type 'a key_parser = ?⁠loc:Loc.t -> 'a option -> vernac_flag_value -> 'a

A parser for some key in an attribute. It is given a nonempty 'a option when the attribute is multiply set for some command.

eg in #[polymorphic] Monomorphic Definition foo := ..., when parsing Monomorphic it will be given Some true.

val attribute_of_list : (string * 'a key_parser) list -> 'a option attribute: Make an attribute from a list of key parsers together with their associated key.

val bool_attribute : name:string -> bool option attribute: Define boolean attribute name, of the form name={yes,no}. The attribute may only be set once for a command.

val qualify_attribute : string -> 'a attribute -> 'a attribute: qualified_attribute qual att treats #[qual(atts)] like att treats atts.

val assert_empty : ?⁠loc:Loc.t -> string -> vernac_flag_value -> unit: assert_empty key v errors if v is not empty. key is used in the error message as the name of the attribute.

val assert_once : ?⁠loc:Loc.t -> name:string -> 'a option -> unit: assert_once ~name v errors if v is not empty. name is used in the error message as the name of the attribute. Used to ensure that a given attribute is not reapeated.

val single_key_parser : name:string -> key:string -> 'a -> 'a key_parser: single_key_parser ~name ~key v makes a parser for attribute name giving the constant value v for key key taking no arguments. name may only be given once.

val make_attribute : (vernac_flags -> vernac_flags * 'a) -> 'a attribute: Make an attribute using the internal representation, thus with access to the full power of attributes. Unstable.

val vernac_polymorphic_flag : Loc.t option -> vernac_flag: Compatibility values for parsing Polymorphic.