Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006365OCamlOCaml typingpublic2014-04-09 05:562014-04-16 08:10
Assigned Togarrigue 
PlatformOSOS Version
Product Version4.02.0+dev 
Target Version4.02.0+devFixed in Version4.02.0+dev 
Summary0006365: "with module" may introduce module alias in signature, this breaks Coq
DescriptionWhen 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.
TagsNo tags attached.
Attached Files

- Relationships
related to 0005514acknowledged "with module" semantics seem broken 

-  Notes
garrigue (manager)
2014-04-09 06:07

Fixed in, 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.
whitequark (developer)
2014-04-16 08:10

@garrigue: the patch broke camlp4 build, see PR6371

- Issue History
Date Modified Username Field Change
2014-04-09 05:56 garrigue New Issue
2014-04-09 05:56 garrigue Status new => assigned
2014-04-09 05:56 garrigue Assigned To => garrigue
2014-04-09 06:05 garrigue Relationship added related to 0005514
2014-04-09 06:07 garrigue Note Added: 0011251
2014-04-09 06:07 garrigue Status assigned => resolved
2014-04-09 06:07 garrigue Fixed in Version => 4.02.0+dev
2014-04-09 06:07 garrigue Resolution open => fixed
2014-04-16 08:10 whitequark Note Added: 0011288

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker