Module ComAssumption

Parameters/Assumptions
val do_assumptions : pstate:Proof_global.t option -> program_mode:bool -> (Decl_kinds.locality * Decl_kinds.polymorphic * Decl_kinds.assumption_object_kind) -> Declaremods.inline -> (Constrexpr.ident_decl list * Constrexpr.constr_expr) Vernacexpr.with_coercion list -> bool
val declare_assumption : pstate:Proof_global.t option -> Vernacexpr.coercion_flag -> Decl_kinds.assumption_kind -> Constr.types Entries.in_universes_entry -> UnivNames.universe_binders -> Impargs.manual_implicits -> bool -> Declaremods.inline -> Names.variable CAst.t -> Names.GlobRef.t * Univ.Instance.t * bool

returns false if the assumption is neither local to a section, nor in a module type and meant to be instantiated.

val do_primitive : Names.lident -> CPrimitives.op_or_type -> Constrexpr.constr_expr option -> unit