Record selectors do not appear with fully qualified names in other modules.

antalsz / hs-to-coq

Convert Haskell source code to Coq source code

https://hs-to-coq.readthedocs.io

MIT License

279 stars 27 forks source link

Record selectors do not appear with fully qualified names in other modules. #55

Closed sweirich closed 6 years ago

sweirich commented 6 years ago

To work around this issue, the midamble for ghc/lib/Name.v includes imports for OccName and Module so that the record selectors defined in these modules will be in scope.