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 quoted_attributes : Attributes.vernac_flags Pcoq.Entry.t
val class_rawexpr : Vernacexpr.class_rawexpr Pcoq.Entry.t
val thm_token : Decls.theorem_kind Pcoq.Entry.t
val def_body : Vernacexpr.definition_expr Pcoq.Entry.t
val decl_notation : Vernacexpr.decl_notation list Pcoq.Entry.t
val record_field : (Vernacexpr.local_decl_expr * Vernacexpr.record_field_attr) Pcoq.Entry.t
val of_type_with_opt_coercion : Vernacexpr.instance_flag 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 add_control_flag : loc:Loc.t -> flag:Vernacexpr.control_flag -> Vernacexpr.vernac_control_r CAst.t -> Vernacexpr.vernac_control_r CAst.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 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