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

Remove deprecated files in Arith and Numbers/Natural #18164

Merged
merged 6 commits into from Nov 28, 2023
Merged

Remove deprecated files in Arith and Numbers/Natural #18164

merged 6 commits into from Nov 28, 2023

Commits on Nov 27, 2023

  1. Remove deprecate files in Arith 

    * Removed in Arith:
  - Div2.v
  - Even.v
  - Gt.v
  - Le.v
  - Lt.v
  - Max.v
  - Minus.v
  - Min.v
  - Mult.v
  - Plus.v
* Removed Numbers/Natural/Peano/NPeano.v
* Many "Require" statements involving these files removed in other parts
  of the library
* Several deprecated lemmas removed in Arith/EqNat
* Register commands moved from Arith_prebase to PeanoNat

* Some test files had to change:

-  bugs/bug_13307.v
-  bugs/bug_1779.v
-  bugs/bug_4187.v
-  bugs/bug_4456.v
-  modules/Nat.v
-  success/Funind.v
-  success/RecTutorial.v
-  success/Require.v (Not sure about this one)
-  success/extraction.v
-  success/import_lib.v
    @Villetaneuse @proux01
    Villetaneuse authored and proux01 committed Nov 27, 2023
    Configuration menu
    Copy the full SHA
    50d8da9 View commit details
    Browse the repository at this point in the history

  2. Remove Arith_prebase 

    The Hint database arith goes in Arith_base
    @Villetaneuse @proux01
    Villetaneuse authored and proux01 committed Nov 27, 2023
    Configuration menu
    Copy the full SHA
    7a325db View commit details
    Browse the repository at this point in the history

  3. Search Blacklist lemmas in Arith_base

    @Villetaneuse @proux01
    Villetaneuse authored and proux01 committed Nov 27, 2023
    Configuration menu
    Copy the full SHA
    a6cfb17 View commit details
    Browse the repository at this point in the history

  4. Remove some entries in doc/stdlib/hidden-files

    @Villetaneuse @proux01
    Villetaneuse authored and proux01 committed Nov 27, 2023
    Configuration menu
    Copy the full SHA
    60c5a2b View commit details
    Browse the repository at this point in the history

  5. Declare last failing jobs of coq#18164 allow_failure 

    So that they can be updated by their devs at their own pace
in the coming weeks.
    @proux01
    proux01 committed Nov 27, 2023
    Configuration menu
    Copy the full SHA
    6e5aefb View commit details
    Browse the repository at this point in the history

  6. Add changelog

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