Adapt w.r.t Coq/Coq#18164

[Villetaneuse]

This prepares the removal of some deprecated files in 8.16.
See coq/coq#18164
Sorry to bother you @ckeller @vblot

[proux01]

@Villetaneuse looking at the long list of commits, I guess this should target the coq-master branch rather than coq-8.13 (you can change that by clicking the "Edit" button on the right of the title on top of the page)

[Villetaneuse]

@Villetaneuse looking at the long list of commits, I guess this should target the coq-master branch rather than coq-8.13 (you can change that by clicking the "Edit" button on the right of the title on top of the page)

Thank you. @SkySkimmer maybe something needs to be updated. I ended up here with make ci-smtcoq. And the "default" branch is 8.13 in smtcoq.

[proux01]

@Villetaneuse looking at the long list of commits, I guess this should target the coq-master branch rather than coq-8.13 (you can change that by clicking the "Edit" button on the right of the title on top of the page)

Thank you. @SkySkimmer maybe something needs to be updated. I ended up here with make ci-smtcoq. And the "default" branch is 8.13 in smtcoq.

Nothing to update (on Coq side at least), there is no reason for the default branch of a repo to be the one used in Coq's CI.

[Villetaneuse]

Just a gentle reminder @ckeller @vblot; could you please consider this PR for smtcoq?

[ckeller]

@Villetaneuse Sorry, I was expecting the usual "please merge now" message (I thought it was the standard?).
I do not know why the workflow fails as it goes through on my pc, merging.

[Villetaneuse]

@Villetaneuse Sorry, I was expecting the usual "please merge now" message (I thought it was the standard?). I do not know why the workflow fails as it goes through on my pc, merging.

Thank you. Sorry if I don't use standard messages, I'm still a bit new to this.

[proux01]

I was expecting the usual "please merge now" message

Just to explain the misunderstanding: there are indeed two kinds of overlays for coq:

• ones that have to be merged in sync with the upstream PR in coq, those are usually the one involving ML code, hence the most commons for plugins like smtcoq
• ones that are backward compatible and should be merged at any time before the upstream PR in coq, those are usually the ones involving .v files, like the current PR

A good practice to avoid confusion is to state explicitly in the top message of the PR which of the two kinds it is and when merge is expected.

[ckeller]

Many thanks @proux01 for claryfying. I will also make sure I understand correctly when a new PR is proposed.
Thank you all for the work!