Skip to content
Snippets Groups Projects

silence some warnings

Merged silence some warnings
wip-warnings into master
All threads resolved!
Merged Björn Brandenburg requested to merge wip-warnings into master
All threads resolved!

Let's make the compilation less noisy.

Merge request reports

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • Björn Brandenburg resolved all threads

    resolved all threads

  • Björn Brandenburg added 2 commits

    added 2 commits

    • 1d28cae3 - Revert "fix unused-intro-pattern warning"
    • a7c84b74 - rewrite proof to fix unused-intro-pattern warning

    Compare with previous version

  • Björn Brandenburg added 1 commit

    added 1 commit

    • ece39eed - fix overlooked deprecation warnings

    Compare with previous version

  • Björn Brandenburg added 3 commits

    added 3 commits

    • 02e7bd4d - silence one redundant canonical projection warning
    • 3813f9ea - rewrite proof to fix unused-intro-pattern warning
    • 699c5b41 - fix overlooked deprecation warnings

    Compare with previous version

  • Björn Brandenburg merged

    merged

    • Please register or sign in to reply