package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type vernac_flag_type =
  1. | FlagIdent of string
  2. | FlagString of string
type vernac_flags = vernac_flag list
and vernac_flag = string * vernac_flag_value
and vernac_flag_value =
  1. | VernacFlagEmpty
  2. | VernacFlagLeaf of vernac_flag_type
  3. | VernacFlagList of vernac_flags
val pr_vernac_flag : vernac_flag -> Pp.t
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 using : string option attribute
val typing_flags : Declarations.typing_flags option 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 -> bool option attribute
val deprecated_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