Module Indschemes.InternalSource

Sourceval do_scheme_all : user_call_scheme:bool -> declare_mind:declare_mind_function -> Libnames.qualid Constrexpr.or_by_notation -> Names.Id.t list option -> unit

Create the All predicate with its theorem all_forall.

Use the reexported function in DeclareInd instead to avoid needing to pass declare_mind.