Module `G_vernac`

val vernac_kw : string list
val query_command : (Goal_select.t option -> Vernacexpr.vernac_expr) Pcoq.Entry.t
val subprf : Vernacexpr.vernac_expr Pcoq.Entry.t
val class_rawexpr : Vernacexpr.class_rawexpr Pcoq.Entry.t
val thm_token : Decl_kinds.theorem_kind Pcoq.Entry.t
val def_body : Vernacexpr.definition_expr Pcoq.Entry.t
val decl_notation : (Names.lstring * Constrexpr.constr_expr * string option) list Pcoq.Entry.t
val record_field : ((Vernacexpr.local_decl_expr Vernacexpr.with_instance * int option) * (Names.lstring * Constrexpr.constr_expr * string option) list) Pcoq.Entry.t
val of_type_with_opt_coercion : bool option Pcoq.Entry.t
val instance_name : (Constrexpr.name_decl * Constrexpr.local_binder_expr list) Pcoq.Entry.t
val section_subset_expr : Vernacexpr.section_subset_expr 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.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