Adapting to Coq PR #14711: Evd.check_univ_decl returns also the universe binders #30
Conversation
|
Is this going to make it into the v8.14 branch? If not, we should split off new compat files |
|
It's a priori for 8.15. I'll create a 8.15 file then, if that's the procedure. |
|
It's a bit more complicated than that, since the Makefile also needs to be modified. If you have trouble figuring out how to do it, I'm happy to make the split myself (probably later today). |
|
The commit that did this for 8.14 is at 4e0ebab ; if you're down to make a separate PR that copies all the v814 files to v815 files and makes the corresponding changes in the Makefile, I'd be happy to merge it; otherwise I'll do it myself shortly |
|
Then, that is probably safer if you do it. Thanks. |
|
Created as #31, I'll merge that once the CI passes |
|
#31 merged, could you rebase this on current master and edit the .v815 file instead of the .v814 one? |
herbelin
force-pushed
the
master+adapt-coq-pr14711-univs-ctx-and-binders-centralized
branch
from
0bd70ea
to
3f2b264
Compare
herbelin
force-pushed
the
master+adapt-coq-pr14711-univs-ctx-and-binders-centralized
branch
from
3f2b264
to
971f000
Compare
|
I pushed, hoping I made it right. Thanks. |
|
Please merge now |
|
@JasonGross ping |
Evd.check_univ_declnow returns also the universe binders by default. We seize the opportunity to propagate them when there are some.To be merged synchronously with coq/coq#14711. Thanks in advance.