ComAssumption (coq-core.ComAssumption)

Parameters/Assumptions

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

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

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

val declare_axiom : 
  Vernacexpr.coercion_flag ->
  poly:bool ->
  local:Locality.import_status ->
  kind:Decls.assumption_object_kind ->
  ?deprecation:Deprecation.t ->
  Constr.types ->
  UState.named_universes_entry ->
  Impargs.manual_implicits ->
  Declaremods.inline ->
  Names.variable CAst.t ->
  Names.GlobRef.t * Univ.Instance.t

Context command

val do_context : poly:bool -> Constrexpr.local_binder_expr list -> unit

val interp_context : 
  Environ.env ->
  Evd.evar_map ->
  Constrexpr.local_binder_expr list ->
  Evd.evar_map
  * (Names.Id.t * Constr.t option * Constr.t * Glob_term.binding_kind) list

The first half of the context command, from expr to constr