Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - chore(*): upgrade to Lean 3.27.0c #6411

Closed
wants to merge 7 commits into from
Closed

[Merged by Bors] - chore(*): upgrade to Lean 3.27.0c #6411

wants to merge 7 commits into from

Commits on Feb 25, 2021

  1. chore(*): upgrade to Lean 3.27.0c

    @robertylewis
    robertylewis committed Feb 25, 2021
    Configuration menu
    Copy the full SHA
    a0208bd View commit details
    Browse the repository at this point in the history

  2. fix from Mario (?)

    @robertylewis
    robertylewis committed Feb 25, 2021
    Configuration menu
    Copy the full SHA
    1bc6fea View commit details
    Browse the repository at this point in the history

  3. name clash

    @robertylewis
    robertylewis committed Feb 25, 2021
    Configuration menu
    Copy the full SHA
    36ea6a6 View commit details
    Browse the repository at this point in the history

  4. fix

    @robertylewis
    robertylewis committed Feb 25, 2021
    Configuration menu
    Copy the full SHA
    ff72779 View commit details
    Browse the repository at this point in the history

  5. unnecessary lines

    @robertylewis
    robertylewis committed Feb 25, 2021
    Configuration menu
    Copy the full SHA
    d35ba10 View commit details
    Browse the repository at this point in the history

  6. golf, thanks Eric

    @robertylewis
    robertylewis committed Feb 25, 2021
    Configuration menu
    Copy the full SHA
    951185d View commit details
    Browse the repository at this point in the history

  7. fix test

    @robertylewis
    robertylewis committed Feb 25, 2021
    Configuration menu
    Copy the full SHA
    782561d View commit details
    Browse the repository at this point in the history