Module DeclareObl.ProgramDecl

type t = private {
prg_name : Names.Id.t;
prg_body : Constr.constr;
prg_type : Constr.constr;
prg_ctx : UState.t;
prg_univdecl : UState.universe_decl;
prg_obligations : obligations;
prg_deps : Names.Id.t list;
prg_fixkind : fixpoint_kind option;
prg_implicits : Impargs.manual_implicits;
prg_notations : Vernacexpr.decl_notation list;
prg_poly : bool;
prg_scope : Declare.locality;
prg_kind : Decls.definition_object_kind;
prg_reduce : Constr.constr -> Constr.constr;
prg_hook : Declare.Hook.t option;
prg_opaque : bool;
}
val make : ?⁠opaque:bool -> ?⁠hook:Declare.Hook.t -> Names.Id.t -> udecl:UState.universe_decl -> uctx:UState.t -> impargs:Impargs.manual_implicits -> poly:bool -> scope:Declare.locality -> kind:Decls.definition_object_kind -> Constr.constr option -> Constr.types -> Names.Id.t list -> fixpoint_kind option -> Vernacexpr.decl_notation list -> (Names.Id.t * Constr.types * Evar_kinds.t Loc.located * (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array -> (Constr.constr -> Constr.constr) -> t
val set_uctx : uctx:UState.t -> t -> t