package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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 unfold_fix : bool attribute
Sourceval locality : bool option 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

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.

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

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

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct