package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val vernac_kw : string list
val query_command : (Goal_select.t option -> Vernacexpr.vernac_expr) Pcoq.Entry.t
val def_body : Vernacexpr.definition_expr Pcoq.Entry.t
val decl_notation : Vernacexpr.decl_notation list Pcoq.Entry.t
val of_type_with_opt_coercion : Vernacexpr.instance_flag Pcoq.Entry.t
val make_bullet : string -> Proof_bullet.t
val parse_compat_version : string -> Flags.compat_version
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 only_starredidentrefs : unit Pcoq.Gram.Entry.e
val starredidentreflist_to_expr : Vernacexpr.section_subset_expr list -> Vernacexpr.section_subset_expr
val warn_deprecated_include_type : ?loc:Loc.t -> unit -> unit