package coq

You can search for identifiers within the package.

in-package search v0.2.0

Formal proof management system

Install

Dune Dependency

coq.inria.fr Edit opam file Versions (38)

Authors

T

The Coq development team, INRIA, CNRS, and contributors.

Maintainers

C

coqdev@inria.fr

Sources

coq-8.14.1.tar.gz

sha256=3cbfc1e1a72b16d4744f5b64ede59586071e31d9c11c811a0372060727bfd9c3

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

Module `ComAssumption`Source

Parameters/Assumptions

Source

val interp_assumption : 
  program_mode:bool ->
  Environ.env ->
  Evd.evar_map ->
  Constrintern.internalization_env ->
  Constrexpr.local_binder_expr list ->
  Constrexpr.constr_expr ->
  Evd.evar_map * EConstr.t * Impargs.manual_implicits

Source

val do_assumptions : 
  program_mode:bool ->
  poly:bool ->
  scope:Locality.locality ->
  kind:Decls.assumption_object_kind ->
  Declaremods.inline ->
  (Constrexpr.ident_decl list * Constrexpr.constr_expr)
    Vernacexpr.with_coercion
    list ->
  unit

Source

val declare_variable : 
  Vernacexpr.coercion_flag ->
  kind:Decls.assumption_object_kind ->
  Constr.types ->
  Impargs.manual_implicits ->
  Glob_term.binding_kind ->
  Names.variable CAst.t ->
  unit

Source

val declare_axiom : 
  Vernacexpr.coercion_flag ->
  poly:bool ->
  local:Locality.import_status ->
  kind:Decls.assumption_object_kind ->
  Constr.types ->
  (Entries.universes_entry * UnivNames.universe_binders) ->
  Impargs.manual_implicits ->
  Declaremods.inline ->
  Names.variable CAst.t ->
  Names.GlobRef.t * Univ.Instance.t

Context command

Sourceval context : poly:bool -> Constrexpr.local_binder_expr list -> unit

On This Page

Parameters/Assumptions

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module ComAssumptionSource

Parameters/Assumptions

Module `ComAssumption`Source