hs-to-coq icon indicating copy to clipboard operation
hs-to-coq copied to clipboard

Published 20 hours ago • verified publisher icon antalsz

Qualify modules under base

Open Lysxia opened this issue 4 years ago • 1 comments

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/.

Lysxia avatar May 30 '20 20:05 Lysxia

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

nomeata avatar Jun 02 '20 08:06 nomeata