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.

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

Remove decimal-only number notations (deprecated in 8.12) #13842

Merged
merged 3 commits into from Mar 5, 2021

Conversation

proux01
Copy link
Contributor

@proux01 proux01 commented Feb 9, 2021

Overlays:

@proux01 proux01 requested review from a team as code owners February 9, 2021 17:26
@Zimmi48 Zimmi48 added this to the 8.14+rc1 milestone Feb 10, 2021
Copy link
Member

@Zimmi48 Zimmi48 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It looks like there are a few projects that still rely on those (cc @JasonGross).

@Zimmi48 Zimmi48 added kind: cleanup Code removal, deprecation, refactorings, etc. needs: changelog entry This should be documented in doc/changelog. labels Feb 10, 2021
@JasonGross
Copy link
Member

I'll update the compatibility files for fiat shortly, when I get a chance

@Zimmi48
Copy link
Member

Zimmi48 commented Feb 10, 2021

What about HoTT? Should we ping someone else?

@JasonGross
Copy link
Member

I expect the overlay for HoTT should be relatively easy to prepare, unlike the one for fiat. I can try to take care of that too, but feel free to look into it if you want it done before I get the chance

proux01 added a commit to proux01/HoTT that referenced this pull request Feb 22, 2021
@proux01
Copy link
Contributor Author

proux01 commented Feb 22, 2021

I expect the overlay for HoTT should be relatively easy to prepare

@JasonGross Indeed, done

JasonGross added a commit to JasonGross/coq-scripts that referenced this pull request Feb 23, 2021
JasonGross added a commit to mit-plv/fiat that referenced this pull request Feb 23, 2021
@JasonGross
Copy link
Member

I've pushed the commit JasonGross/coq-scripts@37c5b72 and mit-plv/fiat@27e5718 so fiat-parsers should work now; I've restarted the pipeline.

@github-actions github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Feb 27, 2021
proux01 added a commit to proux01/HoTT that referenced this pull request Feb 27, 2021
@proux01 proux01 removed the needs: changelog entry This should be documented in doc/changelog. label Feb 27, 2021
@coqbot-app coqbot-app bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Feb 27, 2021
@proux01
Copy link
Contributor Author

proux01 commented Feb 27, 2021

@JasonGross great, thanks.
I added the changelog entry so this should be ready.

@ppedrot ppedrot self-assigned this Feb 27, 2021
@ppedrot
Copy link
Member

ppedrot commented Feb 28, 2021

I'll wait for the HoTT overlay to be merged before merging this one.

proux01 added a commit to proux01/HoTT that referenced this pull request Mar 3, 2021
mikeshulman added a commit to HoTT/Coq-HoTT that referenced this pull request Mar 5, 2021
@ppedrot ppedrot merged commit aacf8f1 into coq:master Mar 5, 2021
@proux01 proux01 deleted the remove-decimal branch March 5, 2021 18:07
andreaslyn pushed a commit to andreaslyn/HoTT that referenced this pull request Mar 31, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: cleanup Code removal, deprecation, refactorings, etc.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

4 participants