Interactive module should error when type is functorized #15348
Labels
kind: user messages
Improvement of error messages, new warnings, etc.
part: modules
The module system of Coq.
current error is on
End M
sayingIncompatible module types: module expects 1 arguments, found 0.
I think we should error on
Module M : T.
(same thing happens for
Module M <: T
)The text was updated successfully, but these errors were encountered: