metacoq icon indicating copy to clipboard operation
metacoq copied to clipboard

Published 20 hours ago • verified publisher icon MetaCoq

Remove Export utils in EAst

Open yforster opened this issue 4 years ago • 3 comments

I'd like to turn this Export into an Import. Otherwise we're running into trouble in CertiCoq: utils export the monad notation globally, which clashes with the monad notation used in coq-ext-lib. That's something which should be fixed anyways, but until then this PR fixes the problem.

yforster avatar Oct 01 '20 12:10 yforster

We still use the Export in erasure apparently :)

mattam82 avatar Oct 02 '20 09:10 mattam82

Still not exactly right, maybe because we merged something else in the meantime ;)

mattam82 avatar Oct 02 '20 17:10 mattam82

Shall we fix this @yforster ?

mattam82 avatar Nov 16 '20 20:11 mattam82