Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - chore: bump Std #10514

Closed
wants to merge 9 commits into from
Closed

Commits on Feb 13, 2024

  1. chore: bump Std

    semorrison committed Feb 13, 2024
    Configuration menu
    Copy the full SHA
    4d68d80 View commit details
    Browse the repository at this point in the history
  2. remove migrated lemmas

    semorrison committed Feb 13, 2024
    Configuration menu
    Copy the full SHA
    dab74b4 View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    631984c View commit details
    Browse the repository at this point in the history
  4. Fix toFin_mul

    tobiasgrosser committed Feb 13, 2024
    Configuration menu
    Copy the full SHA
    e728647 View commit details
    Browse the repository at this point in the history

Commits on Feb 14, 2024

  1. Fix unused import

    tobiasgrosser committed Feb 14, 2024
    Configuration menu
    Copy the full SHA
    0b6e8fd View commit details
    Browse the repository at this point in the history
  2. fixes

    semorrison committed Feb 14, 2024
    Configuration menu
    Copy the full SHA
    b97e3e7 View commit details
    Browse the repository at this point in the history
  3. merge

    semorrison committed Feb 14, 2024
    Configuration menu
    Copy the full SHA
    546b4b3 View commit details
    Browse the repository at this point in the history
  4. resolve mereg conflict

    semorrison committed Feb 14, 2024
    Configuration menu
    Copy the full SHA
    e06f94c View commit details
    Browse the repository at this point in the history
  5. Configuration menu
    Copy the full SHA
    c21533e View commit details
    Browse the repository at this point in the history