Module Attributes

type vernac_flags = vernac_flag list
and vernac_flag = string * vernac_flag_value
and vernac_flag_value =
| VernacFlagEmpty
| VernacFlagLeaf of string
| VernacFlagList of vernac_flags
type +'a attribute
val parse : 'a attribute -> vernac_flags -> 'a
val unsupported_attributes : vernac_flags -> unit
module Notations : sig ... end
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 program_mode_option_name : string list
val only_locality : vernac_flags -> bool option
val only_polymorphism : vernac_flags -> bool
val parse_drop_extra : 'a attribute -> vernac_flags -> 'a
val parse_with_extra : 'a attribute -> vernac_flags -> vernac_flags * 'a
type !'a key_parser = 'a option -> vernac_flag_value -> 'a
val attribute_of_list : (string * 'a key_parser) list -> 'a option attribute
val bool_attribute : name:string -> on:string -> off:string -> bool option attribute
val qualify_attribute : string -> 'a attribute -> 'a attribute
val assert_empty : string -> vernac_flag_value -> unit
val assert_once : name:string -> 'a option -> unit
val single_key_parser : name:string -> key:string -> 'a -> 'a key_parser
val make_attribute : (vernac_flags -> vernac_flags * 'a) -> 'a attribute
val vernac_polymorphic_flag : vernac_flag
val vernac_monomorphic_flag : vernac_flag
val universe_polymorphism_option_name : string list
val is_universe_polymorphism : unit -> bool