avoid warnings emitted by Coq #76
Conversation
|
Sorry to be late, but now, it seems that there are still some warnings, and moreover, it fails on: A version problem? |
ybertot
force-pushed
the
coq-deprecation-8.13
branch
from
cf22d16
to
ec2d8bf
Compare
|
After git rebase, it seems the error has disappeared. |
|
Only the test-suite fails, and it seems this is only due to re-ordering in the graph. |
|
What about merging your other PR into this one and updating the oracles? Sorry, but I prefer not to merge a branch where the tests fail... |
|
I agree on the point concerning not merging a branch where tests fails. |
|
Some of the changes cannot be fixed by sorting results. It seems there was a symbol for the section variable A that was removed and it shifts the indices of all nodes (this is for the graph.dpd file). |
|
OK, but if it looks "normal" (I mean, due to coq internal modifications), you can just copy the new results in the oracles, and it will be ok then. |
|
I agree, I am checking the normalcy of the graph just now. |
Only modifications in the Coq source files.