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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - refactor(order/filter): refactor filters infi and bases #2384

Closed
wants to merge 9 commits into from
Closed

[Merged by Bors] - refactor(order/filter): refactor filters infi and bases #2384

wants to merge 9 commits into from

Commits on Apr 10, 2020

  1. Refactor filters infi and bases

    @PatrickMassot
    PatrickMassot committed Apr 10, 2020
    Configuration menu
    Copy the full SHA
    56cfb29 View commit details
    Browse the repository at this point in the history

  2. Apply suggestions from code review 

    Co-Authored-By: Gabriel Ebner <gebner@gebner.org>
    @PatrickMassot @gebner
    PatrickMassot and gebner committed Apr 10, 2020
    Configuration menu
    Copy the full SHA
    78a1c2e View commit details
    Browse the repository at this point in the history

  3. Update src/order/filter/bases.lean 

    Fix Gabriel's fix
    @PatrickMassot
    PatrickMassot committed Apr 10, 2020
    Configuration menu
    Copy the full SHA
    2bf68ea View commit details
    Browse the repository at this point in the history

  4. Apply suggestions from code review 

    Co-Authored-By: Johan Commelin <johan@commelin.net>
    @PatrickMassot @jcommelin
    PatrickMassot and jcommelin committed Apr 10, 2020
    Configuration menu
    Copy the full SHA
    7dd9ae4 View commit details
    Browse the repository at this point in the history

Commits on Apr 11, 2020

  1. Apply suggestions from code review 

    Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>
    @PatrickMassot @sgouezel
    PatrickMassot and sgouezel committed Apr 11, 2020
    Configuration menu
    Copy the full SHA
    ca26894 View commit details
    Browse the repository at this point in the history

  2. Describe the example filter bases

    @PatrickMassot
    PatrickMassot committed Apr 11, 2020
    Configuration menu
    Copy the full SHA
    70c71b8 View commit details
    Browse the repository at this point in the history

Commits on Apr 12, 2020

  1. Missing typo fix

    @PatrickMassot
    PatrickMassot committed Apr 12, 2020
    Configuration menu
    Copy the full SHA
    49e1525 View commit details
    Browse the repository at this point in the history

  2. Remove uneeded prime

    @PatrickMassot
    PatrickMassot committed Apr 12, 2020
    Configuration menu
    Copy the full SHA
    d7a8d9e View commit details
    Browse the repository at this point in the history

Commits on Apr 13, 2020

  1. Merge branch 'master' into filter-bases-pr

    @sgouezel
    sgouezel committed Apr 13, 2020
    Configuration menu
    Copy the full SHA
    6e63ae7 View commit details
    Browse the repository at this point in the history