everparse icon indicating copy to clipboard operation
everparse copied to clipboard

Published 20 hours ago • verified publisher icon project-everest

Fixes for FStarLang/FStar#1905

Open mtzguido opened this issue 5 years ago • 1 comments

This PR fixes spurious uses of names, as described in FStarLang/FStar#1905. F* will reject these names with a syntax error once the fix is merged (waiting on this PR and one in miTLS).

mtzguido avatar Mar 19 '20 16:03 mtzguido

F* now just warns for these things, so this PR is just to remove the warnings. (So if this conflicts with #9, I think you should favour that PR.)

mtzguido avatar Apr 13 '20 14:04 mtzguido