Skip to content

Replace unused pattern variables with underscore

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

Addresses new unused-pattern-matching-variable warning on Coq master (see

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 by Tej Chajed

Merge request reports