Up – Package index » rocq-runtime » Library rocq-runtime.engine » Evd » MiniEConstr » ERelevance

Module `MiniEConstr.ERelevance`Source

Sourcetype t = erelevance

Sourceval make : Sorts.relevance -> t

Sourceval kind : evar_map -> t -> Sorts.relevance

Sourceval unsafe_to_relevance : t -> Sorts.relevance