Coq_checklib.CheckTypes
val check_polymorphic_arity : Environ.env -> Constr.rel_context -> Declarations.template_universes -> unit