Join GitHub today
GitHub is home to over 31 million developers working together to host and review code, manage projects, and build software together.Sign up
"with module" may introduce module alias in signature, this breaks Coq #6365
Original bug ID: 6365
When N is a module alias, the construction "S with module M = N" introduces this alias in the resulting signature.
Comment author: @garrigue
Fixed in typemod.ml, by applying Mtype.remove_alias to the inserted signature.
Note that this is related to 5514: the official semantics is not to insert the signature of the right-hand side of the equation, but just add equations to the contained types.