package coq

  1. Overview
  2. Docs
Formal proof management system

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (40)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors.

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.16.1.tar.gz
sha256=583471c8ed4f227cb374ee8a13a769c46579313d407db67a82d202ee48300e4b

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

Module AttributesSource

Sourcetype vernac_flag_type =
  1. | FlagIdent of string
  2. | 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 =
  1. | VernacFlagEmpty
  2. | VernacFlagLeaf of vernac_flag_type
  3. | 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 locality : bool option attribute
Sourceval deprecation : Deprecation.t option attribute
Sourceval reversible : bool option attribute
Sourceval canonical_field : bool attribute
Sourceval canonical_instance : bool attribute
Sourceval using : string option attribute
Sourceval hint_locality : default:(unit -> Hints.hint_locality) -> Hints.hint_locality attribute
Sourceval really_hint_locality : Hints.hint_locality attribute

With the warning for Hint (and not for Instance etc)

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.

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