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

avoid warnings emitted by Coq #76

Open
wants to merge 3 commits into
base: coq-master
Choose a base branch
from

Conversation

ybertot
Copy link
Collaborator

@ybertot ybertot commented Sep 24, 2020

Only modifications in the Coq source files.

@Karmaki
Copy link
Collaborator

Karmaki commented Oct 29, 2020

Sorry to be late, but now, it seems that there are still some warnings, and moreover, it fails on:

Error: Unbound module Names.GlobRef.Ordered_env

A version problem?

@ybertot
Copy link
Collaborator Author

ybertot commented Oct 29, 2020

After git rebase, it seems the error has disappeared.

@ybertot
Copy link
Collaborator Author

ybertot commented Oct 30, 2020

Only the test-suite fails, and it seems this is only due to re-ordering in the graph.

@Karmaki
Copy link
Collaborator

Karmaki commented Oct 30, 2020

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...

@ybertot
Copy link
Collaborator Author

ybertot commented Oct 30, 2020

I agree on the point concerning not merging a branch where tests fails.

@ybertot
Copy link
Collaborator Author

ybertot commented Oct 30, 2020

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).

@Karmaki
Copy link
Collaborator

Karmaki commented Oct 30, 2020

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.

@ybertot
Copy link
Collaborator Author

ybertot commented Oct 30, 2020

I agree, I am checking the normalcy of the graph just now.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants