You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Original bug ID: 6365 Reporter:@garrigue Assigned to:@garrigue Status: closed (set by @xavierleroy on 2015-12-11T18:26:35Z) Resolution: fixed Priority: normal Severity: minor Version: 4.02.0+dev Target version: 4.02.0+dev Fixed in version: 4.02.0+dev Category: typing Related to:#5514
Bug description
When N is a module alias, the construction "S with module M = N" introduces this alias in the resulting signature.
As a result compilation of the trunk version of coq is broken.
The text was updated successfully, but these errors were encountered:
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.
Original bug ID: 6365
Reporter: @garrigue
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2015-12-11T18:26:35Z)
Resolution: fixed
Priority: normal
Severity: minor
Version: 4.02.0+dev
Target version: 4.02.0+dev
Fixed in version: 4.02.0+dev
Category: typing
Related to: #5514
Bug description
When N is a module alias, the construction "S with module M = N" introduces this alias in the resulting signature.
As a result compilation of the trunk version of coq is broken.
The text was updated successfully, but these errors were encountered: