ComAssumptionSourceval 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_implicitsval 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 ->
unitval declare_variable :
Vernacexpr.coercion_flag ->
kind:Decls.assumption_object_kind ->
Constr.types ->
Impargs.manual_implicits ->
Glob_term.binding_kind ->
Names.variable CAst.t ->
unitval 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.tContext command