Module `Attributes`Source

Sourcetype vernac_flag_type =

| FlagIdent of string
| FlagString of string

The type of parsing attribute data

Sourcetype vernac_flags = vernac_flag list

Sourceand vernac_flag = (string * vernac_flag_value) CAst.t

Sourceand vernac_flag_value =

| VernacFlagEmpty
| VernacFlagLeaf of vernac_flag_type
| VernacFlagList of vernac_flags

Sourceval pr_vernac_flag : vernac_flag -> Pp.t

Sourcetype +'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.

Sourceval parse : 'a attribute -> vernac_flags -> 'a

Errors on unsupported attributes.

Sourceval unsupported_attributes : vernac_flags -> unit

Errors if the list of flags is nonempty.

Sourcemodule Notations : sig ... end

Notations to combine attributes.

Definitions for some standard attributes.

Sourceval raw_attributes : vernac_flags attribute

Sourceval polymorphic : bool attribute

Sourceval program : bool attribute

Sourceval template : bool option attribute

Sourceval unfold_fix : bool attribute

Sourceval locality : bool option attribute

Sourceval option_locality : Goptions.option_locality attribute

Sourceval deprecation : Deprecation.t option attribute

Sourceval user_warn_warn : UserWarn.warn list attribute

Sourceval user_warns : UserWarn.t option attribute

Sourceval reversible : bool option attribute

Sourceval canonical_field : bool attribute

Sourceval canonical_instance : bool attribute

Sourceval using : string option attribute

Sourceval explicit_hint_locality : Hints.hint_locality option attribute

Sourceval bind_scope_where : Notation.add_scope_where option attribute

Sourceval hint_locality : Hints.hint_locality attribute

Default: if sections are opened then Local otherwise Export. Although this is named and uses the type hint_locality it may be used as the standard 3-valued locality attribute.

Sourceval typing_flags : Declarations.typing_flags option attribute

Enable/Disable universe checking

Sourceval program_mode_option_name : string list

For internal use when messing with the global option.

Sourceval only_locality : vernac_flags -> bool option

Parse attributes allowing only locality.

Sourceval only_polymorphism : vernac_flags -> bool

Parse attributes allowing only polymorphism. Uses the global flag for the default value.

Sourceval parse_drop_extra : 'a attribute -> vernac_flags -> 'a

Ignores unsupported attributes.

Sourceval parse_with_extra : 'a attribute -> vernac_flags -> vernac_flags * 'a

Returns unsupported attributes.

* Defining attributes.

Sourcetype '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.

Sourceval 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.

Source

val payload_parser : 
  ?cat:(string -> string -> string) ->
  name:string ->
  string key_parser

payload_parser ?cat ~name parses attributes like #[name="payload"]. If the attribute is used multiple times and cat is non-None, the payloads are concatenated using it. If cat is None, having multiple occurences of the attribute is forbidden.

Source

val payload_attribute : 
  ?cat:(string -> string -> string) ->
  name:string ->
  string option attribute

This is just attribute_of_list for a single payload_parser.

Sourceval 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.

Sourceval qualify_attribute : string -> 'a attribute -> 'a attribute

qualified_attribute qual att treats #[qual(atts)] like att treats atts.

Combinators to help define your own parsers. See the implementation of bool_attribute for practical use.

Sourceval 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.

Sourceval 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.

Sourceval 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.

Sourceval 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.

Sourceval vernac_polymorphic_flag : Loc.t option -> vernac_flag

Compatibility values for parsing Polymorphic.

Sourceval vernac_monomorphic_flag : Loc.t option -> vernac_flag

Sourceval universe_polymorphism_option_name : string list

For internal use.

Sourceval is_universe_polymorphism : unit -> bool

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.vernac/Attributes/index.html

Module `Attributes`Source

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.vernac/Attributes/index.html

Module AttributesSource

Module `Attributes`Source