This repository has been archived by the owner on Nov 17, 2020. It is now read-only.

Qualify modules under base #158

Open

Lysxia opened this issue May 30, 2020 · 1 comment

Contributor

Lysxia commented May 30, 2020

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

The text was updated successfully, but these errors were encountered:

Collaborator

nomeata commented Jun 2, 2020

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

lastland mentioned this issue

Qualify modules under base plclub/hs-to-coq#158

Closed

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.