Module `G_vernac`Source

val query_command : 
  (Goal_select.t option -> Vernacexpr.synpure_vernac_expr) Procq.Entry.t

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

val search_queries : 
  ((bool * Vernacexpr.search_request) list
   * Libnames.qualid list Vernacexpr.search_restriction)
    Procq.Entry.t

Sourceval subprf : Vernacexpr.synpure_vernac_expr Procq.Entry.t

val subprf_with_selector : 
  (Goal_select.t option -> Vernacexpr.synpure_vernac_expr) Procq.Entry.t

Sourceval quoted_attributes : Attributes.vernac_flags Procq.Entry.t

Sourceval coercion_class : Vernacexpr.coercion_class Procq.Entry.t

Sourceval thm_token : Decls.theorem_kind Procq.Entry.t

val def_token : 
  (Vernacexpr.discharge * Decls.definition_object_kind) Procq.Entry.t

val assumption_token : 
  (Vernacexpr.discharge * Decls.assumption_object_kind) Procq.Entry.t

Sourceval def_body : Vernacexpr.definition_expr Procq.Entry.t

Sourceval notation_declaration : Vernacexpr.notation_declaration Procq.Entry.t

Sourceval decl_notations : Vernacexpr.notation_declaration list Procq.Entry.t

val record_field : 
  (Vernacexpr.local_decl_expr * Vernacexpr.record_field_attr_unparsed)
    Procq.Entry.t

Sourceval of_type : Vernacexpr.coercion_flag Procq.Entry.t

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

Sourceval section_subset_expr : Vernacexpr.section_subset_expr Procq.Entry.t

Sourceval scope_delimiter : Vernacexpr.scope_delimiter Procq.Entry.t

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

Sourceval make_bullet : string -> Proof_bullet.t

Sourceval test_hash_ident : unit Procq.Entry.t

Sourceval test_id_colon : unit Procq.Entry.t

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

Sourceval test_variance_ident : unit Procq.Entry.t

Sourceval test_only_starredidentrefs : unit Procq.Entry.t

Sourceval goal_selector : Goal_select.t Procq.Entry.t

Sourceval toplevel_selector : Goal_select.t Procq.Entry.t

Install