Replace unused pattern variables with underscore (!203) · Merge requests · Iris / stdpp · GitLab

Snippets Groups Projects

Merged Tej Chajed requested to merge tchajed/stdpp:fix-unused-variable-warnings into master 4 years ago

All threads resolved!

Addresses new unused-pattern-matching-variable warning on Coq master (see https://github.com/coq/coq/pull/12768).

I'm pretty sure the hlist.v warning is a bug in Coq's heuristics for this, since those variables are used as implicit arguments and I don't see why the pattern matches more than one case (the warning is also printed twice for the same definition). Maybe there's something in the elaborated term I'm missing, which Coq doesn't even print back?

Regardless of what's going on in Coq, it's much easier for us to suppress the warning than to try to fix this upstream.

Edited 4 years ago by Tej Chajed

Activity

Robbert Krebbers @robbertkrebbers started a thread on an old version of the diff 4 years ago

Resolved 4 years ago by Robbert Krebbers
Last reply by Robbert Krebbers 4 years ago

Tej Chajed @tchajed started a thread on an old version of the diff 4 years ago

Resolved 4 years ago by Tej Chajed

Tej Chajed added 1 commit 4 years ago

added 1 commit

b920e707 - Replace unused pattern variables with underscore

Compare with previous version

Tej Chajed resolved all threads 4 years ago

resolved all threads

Tej Chajed changed title from Prefix unused pattern variables with underscore to Replace unused pattern variables with underscore 4 years ago

changed title from Prefix unused pattern variables with underscore to Replace unused pattern variables with underscore

Robbert Krebbers @robbertkrebbers · 4 years ago

Owner

Oops, I somehow missed that you updated this MR. Merging now. Many thanks!

Robbert Krebbers merged 4 years ago

merged

Robbert Krebbers mentioned in commit 4 years ago

mentioned in commit 41b8ca41

Please register or sign in to reply