package coq-core
Install
Dune Dependency
Authors
Maintainers
Sources
md5=66e57ea55275903bef74d5bf36fbe0f1
sha512=1a7eac6e2f58724a3f9d68bbb321e4cfe963ba1a5551b9b011db4b3f559c79be433d810ff262593d753770ee41ea68fbd6a60daa1e2319ea00dff64c8851d70b
doc/coq-core.vernac/Attributes/index.html
Module Attributes
Source
The type of parsing attribute data
and vernac_flag_value =
| VernacFlagEmpty
| VernacFlagLeaf of vernac_flag_type
| VernacFlagList of vernac_flags
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.
Errors on unsupported attributes.
Errors if the list of flags is nonempty.
Definitions for some standard attributes.
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.
Enable/Disable universe checking
For internal use when messing with the global option.
Parse attributes allowing only locality.
Parse attributes allowing only polymorphism. Uses the global flag for the default value.
Ignores unsupported attributes.
Returns unsupported attributes.
* Defining attributes.
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
.
Make an attribute from a list of key parsers together with their associated key.
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.
val payload_attribute :
?cat:(string -> string -> string) ->
name:string ->
string option attribute
This is just attribute_of_list
for a single payload_parser
.
Define boolean attribute name
, of the form name={yes,no}
. The attribute may only be set once for a command.
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.
assert_empty key v
errors if v
is not empty. key
is used in the error message as the name of the attribute.
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.
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.
Make an attribute using the internal representation, thus with access to the full power of attributes. Unstable.
Compatibility values for parsing Polymorphic
.
For internal use.