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] - doc(Algebra,AlgebraicGeometry): remove mathlib3 names in doc comments #11955

Closed
wants to merge 8 commits into from
Closed

[Merged by Bors] - doc(Algebra,AlgebraicGeometry): remove mathlib3 names in doc comments #11955

wants to merge 8 commits into from

Commits on Apr 6, 2024

  1. doc(Algebra,AlgebraicGeometry): remove mathlib3 names in doc comments 

    Mostly automatic, with a few manual corrections.
    @grunweg
    grunweg committed Apr 6, 2024
    Configuration menu
    Copy the full SHA
    78cdacd View commit details
    Browse the repository at this point in the history

Commits on Apr 7, 2024

  1. Merge branch 'master' into MR-algebraX-mathlib3-docs

    @grunweg
    grunweg committed Apr 7, 2024
    Configuration menu
    Copy the full SHA
    3c6aad2 View commit details
    Browse the repository at this point in the history

  2. Manual fix-ups.

    @grunweg
    grunweg committed Apr 7, 2024
    Configuration menu
    Copy the full SHA
    205d775 View commit details
    Browse the repository at this point in the history

  3. Fix line length.

    @grunweg
    grunweg committed Apr 7, 2024
    Configuration menu
    Copy the full SHA
    8c9fbbb View commit details
    Browse the repository at this point in the history

  4. Apply suggestions from code review 

    Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
    @grunweg @Ruben-VandeVelde
    grunweg and Ruben-VandeVelde committed Apr 7, 2024
    Configuration menu
    Copy the full SHA
    3ef5392 View commit details
    Browse the repository at this point in the history

  5. One more.

    @grunweg
    grunweg committed Apr 7, 2024
    Configuration menu
    Copy the full SHA
    0ef6ba3 View commit details
    Browse the repository at this point in the history

  6. Revert one more.

    @grunweg
    grunweg committed Apr 7, 2024
    Configuration menu
    Copy the full SHA
    1f4e733 View commit details
    Browse the repository at this point in the history

  7. chore(Algebra/Category/Ring/FilteredColimits): remaining changes

    @grunweg
    grunweg committed Apr 7, 2024
    Configuration menu
    Copy the full SHA
    891702c View commit details
    Browse the repository at this point in the history