Module Declare.Info

Information for a declaration, interactive or not, includes parameters shared by mutual constants

type t
val make : ?⁠poly:bool -> ?⁠inline:bool -> ?⁠kind:Decls.logical_kind -> ?⁠udecl:UState.universe_decl -> ?⁠scope:Locality.locality -> ?⁠hook:Hook.t -> ?⁠typing_flags:Declarations.typing_flags -> unit -> t

Note that opaque doesn't appear here as it is not known at the start of the proof in the interactive case.