package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
module C = Constr
val query_command : (Goal_select.t option -> Vernacexpr.vernac_expr) Pcoq.Entry.t
val search_query : (bool * Vernacexpr.search_request) Pcoq.Entry.t
val quoted_attributes : Attributes.vernac_flags Pcoq.Entry.t
val def_body : Vernacexpr.definition_expr Pcoq.Entry.t
val decl_notations : Vernacexpr.decl_notation list Pcoq.Entry.t
val scope_delimiter : Vernacexpr.scope_name Pcoq.Entry.t
val syntax_modifiers : Vernacexpr.syntax_modifier CAst.t list Pcoq.Entry.t
val make_bullet : string -> Proof_bullet.t
val test_hash_ident : unit Pcoq.Entry.t
val test_id_colon : unit Pcoq.Entry.t
val warn_plural_command : ?loc:Loc.t -> string -> unit
val test_plural_form : Loc.t -> string -> ('a * ('b list * 'c)) list -> unit
val test_plural_form_types : Loc.t -> string -> ('a list * 'b) list -> unit
val lname_of_lident : Names.lident -> Names.lname
val name_of_ident_decl : Constrexpr.ident_decl -> Constrexpr.name_decl
val test_variance_ident : unit Pcoq.Entry.t
val test_only_starredidentrefs : unit Pcoq.Entry.t
val starredidentreflist_to_expr : Vernacexpr.section_subset_expr list -> Vernacexpr.section_subset_expr
val warn_deprecated_include_type : ?loc:Loc.t -> unit -> unit
val warn_deprecated_as_ident_kind : ?loc:Loc.t -> unit -> unit
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