Module G_vernac

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