Module `ComAssumption`

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.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: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.t