package coq-core

You can search for identifiers within the package.

in-package search v0.2.0

The Coq Proof Assistant -- Core Binaries and Tools

Install

dune-project

Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

T

The Coq development team, INRIA, CNRS, and contributors

Maintainers

T

The Coq development team <coqdev@inria.fr>

Sources

coq-8.18.0.tar.gz

md5=8d852367b54f095d9fbabd000304d450

sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50

doc/coq-core.vernac/G_vernac/index.html

Module `G_vernac`Source

Source

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

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

Source

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

Sourceval subprf : Vernacexpr.synpure_vernac_expr Pcoq.Entry.t

Sourceval quoted_attributes : Attributes.vernac_flags Pcoq.Entry.t

Sourceval coercion_class : Vernacexpr.coercion_class Pcoq.Entry.t

Sourceval thm_token : Decls.theorem_kind Pcoq.Entry.t

Source

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

Source

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

Sourceval def_body : Vernacexpr.definition_expr Pcoq.Entry.t

Sourceval notation_declaration : Vernacexpr.notation_declaration Pcoq.Entry.t

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

Source

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

Sourceval of_type : Vernacexpr.coercion_flag Pcoq.Entry.t

Source

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

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_variance_ident : unit Pcoq.Entry.t

Sourceval test_only_starredidentrefs : unit Pcoq.Entry.t

package coq-core

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/coq-core.vernac/G_vernac/index.html

Module G_vernacSource

dune-project
Dependency

Module `G_vernac`Source