Module `G_vernac`Source

module C = Constr

val query_command : 
  (Goal_select.t option -> Vernacexpr.vernac_expr) Pcoq.Entry.t

Sourceval search_query : (bool * Vernacexpr.search_request) Pcoq.Entry.t

val search_queries : 
  ((bool * Vernacexpr.search_request) list * Vernacexpr.search_restriction)
    Pcoq.Entry.t

Sourceval subprf : Vernacexpr.vernac_expr Pcoq.Entry.t

Sourceval quoted_attributes : Attributes.vernac_flags Pcoq.Entry.t

Sourceval class_rawexpr : Vernacexpr.class_rawexpr Pcoq.Entry.t

Sourceval 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

Sourceval def_body : Vernacexpr.definition_expr Pcoq.Entry.t

Sourceval decl_notations : Vernacexpr.decl_notation list Pcoq.Entry.t

val record_field : 
  (Vernacexpr.local_decl_expr * Vernacexpr.record_field_attr) Pcoq.Entry.t

Sourceval of_type : Vernacexpr.coercion_flag Pcoq.Entry.t

val of_type_inst : 
  (Vernacexpr.coercion_flag * Vernacexpr.instance_flag) Pcoq.Entry.t

Sourceval section_subset_expr : Vernacexpr.section_subset_expr Pcoq.Entry.t

Sourceval scope_delimiter : Vernacexpr.scope_name Pcoq.Entry.t

Sourceval syntax_modifiers : Vernacexpr.syntax_modifier CAst.t list Pcoq.Entry.t

Sourceval 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

Sourceval test_hash_ident : unit Pcoq.Entry.t

Sourceval test_id_colon : unit Pcoq.Entry.t

Sourceval warn_plural_command : ?loc:Loc.t -> string -> unit

Sourceval test_plural_form : Loc.t -> string -> ('a * ('b list * 'c)) list -> unit

Sourceval test_plural_form_types : Loc.t -> string -> ('a list * 'b) list -> unit

Sourceval lname_of_lident : Names.lident -> Names.lname

Sourceval name_of_ident_decl : Constrexpr.ident_decl -> Constrexpr.name_decl

Sourceval test_variance_ident : unit Pcoq.Entry.t

Sourceval test_only_starredidentrefs : unit Pcoq.Entry.t

val starredidentreflist_to_expr : 
  Vernacexpr.section_subset_expr list ->
  Vernacexpr.section_subset_expr

Sourceval warn_deprecated_include_type : ?loc:Loc.t -> unit -> unit

Sourceval warn_deprecated_as_ident_kind : ?loc:Loc.t -> unit -> unit

Install