Module `ComAssumption`

val do_assumptions : program_mode:bool -> poly:bool -> scope:DeclareDef.locality -> kind:Decls.assumption_object_kind -> 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 -> Impargs.manual_implicits -> Glob_term.binding_kind -> Names.variable CAst.t -> unit
val declare_axiom : Vernacexpr.coercion_flag -> poly:bool -> local:Declare.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

val context : poly:bool -> Constrexpr.local_binder_expr list -> unit
val declare_assumption : Vernacexpr.coercion_flag -> poly:bool -> scope:DeclareDef.locality -> kind:Decls.assumption_object_kind -> Constr.types -> Entries.universes_entry -> UnivNames.universe_binders -> Impargs.manual_implicits -> Glob_term.binding_kind -> Declaremods.inline -> Names.variable CAst.t -> Names.GlobRef.t * Univ.Instance.t: Deprecated