Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Register
  • Sign in
  • S stdpp
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 84
    • Issues 84
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 9
    • Merge requests 9
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • stdpp
  • Merge requests
  • !203

Replace unused pattern variables with underscore

  • Review changes

  • Download
  • Patches
  • Plain diff
Merged Tej Chajed requested to merge tchajed/stdpp:fix-unused-variable-warnings into master Nov 21, 2020
  • Overview 8
  • Commits 1
  • Pipelines 0
  • Changes 2

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 Nov 23, 2020 by Tej Chajed
Assignee
Assign to
Reviewers
Request review from
Time tracking
Source branch: fix-unused-variable-warnings