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] - chore(Topology/PartialHomeomorph): minor clean-up #9633

Closed
wants to merge 11 commits into from
Closed

[Merged by Bors] - chore(Topology/PartialHomeomorph): minor clean-up #9633

wants to merge 11 commits into from

Commits on Jan 10, 2024

  1. Re-use.

    @grunweg
    grunweg committed Jan 10, 2024
    Configuration menu
    Copy the full SHA
    406c485 View commit details
    Browse the repository at this point in the history

  2. Add some sections to the file, making the grouping of lemmas clearer. 

    And avoid some variable binder update.
    @grunweg
    grunweg committed Jan 10, 2024
    Configuration menu
    Copy the full SHA
    9383524 View commit details
    Browse the repository at this point in the history

  3. Move one section further down: first products, then piecewise stuff.

    @grunweg
    grunweg committed Jan 10, 2024
    Configuration menu
    Copy the full SHA
    3a5d587 View commit details
    Browse the repository at this point in the history

Commits on Jan 11, 2024

  1. Merge branch 'master' into MR-topology.partialhomeo-cleanup

    @grunweg
    grunweg committed Jan 11, 2024
    Configuration menu
    Copy the full SHA
    f2130e5 View commit details
    Browse the repository at this point in the history

Commits on Jan 12, 2024

  1. Merge branch 'master' into MR-topology.partialhomeo-cleanup

    @grunweg
    grunweg committed Jan 12, 2024
    Configuration menu
    Copy the full SHA
    a6dd9f6 View commit details
    Browse the repository at this point in the history

Commits on Jan 16, 2024

  1. Merge branch 'master' into MR-topology.partialhomeo-cleanup

    @grunweg
    grunweg committed Jan 16, 2024
    Configuration menu
    Copy the full SHA
    44da397 View commit details
    Browse the repository at this point in the history

  2. Blank lines; remove one unused open statement.

    @grunweg
    grunweg committed Jan 16, 2024
    Configuration menu
    Copy the full SHA
    6b87882 View commit details
    Browse the repository at this point in the history

Commits on Jan 19, 2024

  1. Style fixes: full stops, minor grammar etc.

    @grunweg
    grunweg committed Jan 19, 2024
    Configuration menu
    Copy the full SHA
    3186db5 View commit details
    Browse the repository at this point in the history

  2. Review comments.

    @grunweg
    grunweg committed Jan 19, 2024
    Configuration menu
    Copy the full SHA
    9556015 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into MR-topology.partialhomeo-cleanup

    @grunweg
    grunweg committed Jan 19, 2024
    Configuration menu
    Copy the full SHA
    e0e134f View commit details
    Browse the repository at this point in the history

  4. Revert changes to HausdorffDistance, oops.

    @grunweg
    grunweg committed Jan 19, 2024
    Configuration menu
    Copy the full SHA
    a64a1c0 View commit details
    Browse the repository at this point in the history