Closed mtzguido closed 1 year ago
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 Everparse).
Sorry, apparently I've missed some more, don't merge yet.
Should be good now. F* will actually warn instead of failing, so this PR removes the warnings.
This is pretty stale by now, and not a big deal.
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 Everparse).