package coq

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 ->
  UState.named_universes_entry ->
  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 ->
  UState.named_universes_entry ->
  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-project Dependency

Authors

Maintainers

Sources

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

Module ComAssumptionSource

Parameters/Assumptions

dune-project
Dependency

Module `ComAssumption`Source