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

Support for deprecating a file #18193

Merged
merged 4 commits into from Nov 23, 2023
Merged

Support for deprecating a file #18193

merged 4 commits into from Nov 23, 2023

Commits on Nov 23, 2023

  1. Command "Attributes attributes" to bind attributes to a file. 

    The attribute "deprecated" is supported.

Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
    @herbelin @jfehrle @proux01
    2 people authored and proux01 committed Nov 23, 2023
    Configuration menu
    Copy the full SHA
    ce5ea84 View commit details
    Browse the repository at this point in the history

  2. Add tests for Library Attributes

    @proux01
    proux01 committed Nov 23, 2023
    Configuration menu
    Copy the full SHA
    ea9f4bd View commit details
    Browse the repository at this point in the history

  3. Documenting in passing that attributes deprecated applies to Definiti… 

    …on & cie.
    @herbelin @proux01
    herbelin authored and proux01 committed Nov 23, 2023
    Configuration menu
    Copy the full SHA
    9d85c9f View commit details
    Browse the repository at this point in the history

  4. Change log for coq#18193

    @herbelin @proux01
    herbelin authored and proux01 committed Nov 23, 2023
    Configuration menu
    Copy the full SHA
    56c4e51 View commit details
    Browse the repository at this point in the history