Qualify modules under base

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

Open Lysxia opened 4 years ago

Lysxia commented 4 years ago

Right now the Coq code is compiled with -R base/ "", which causes warnings because these modules have the same names as those under base-thy/.

nomeata commented 4 years ago

That was a design choice back then (and we learned to live with the warning). Maybe not very Coq’ish, so of course can be changed