Module `G_vernac`

val query_command : (Goal_select.t option -> Vernacexpr.vernac_expr) Pcoq.Entry.t
val search_query : (bool * Vernacexpr.search_request) Pcoq.Entry.t
val search_queries : ((bool * Vernacexpr.search_request) list * Vernacexpr.search_restriction) 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_token : (Vernacexpr.discharge * Decls.definition_object_kind) Pcoq.Entry.t
val assumption_token : (Vernacexpr.discharge * Decls.assumption_object_kind) Pcoq.Entry.t
val def_body : Vernacexpr.definition_expr Pcoq.Entry.t
val decl_notations : 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 scope_delimiter : Vernacexpr.scope_name Pcoq.Entry.t
val syntax_modifiers : Vernacexpr.syntax_modifier list Pcoq.Entry.t
val only_parsing : bool Pcoq.Entry.t
val make_bullet : string -> Proof_bullet.t
val add_control_flag : loc:Loc.t -> flag:Vernacexpr.control_flag -> Vernacexpr.vernac_control_r CAst.t -> Vernacexpr.vernac_control_r CAst.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_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