Inductiveops.Internal
val nf_relevance : Evd.evar_map -> Sorts.relevance -> Sorts.relevance
val should_invert_case : Environ.env -> Evd.evar_map -> Sorts.relevance -> Constr.case_info -> bool