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.

Sign up for GitHub

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

Jump to bottom

Cannot add monomorphic constraints #708

Open

rtetley opened this issue Jan 17, 2024 · 1 comment

Labels

bug

Collaborator

rtetley commented Jan 17, 2024

This issue was reported on zulip here: https://coq.zulipchat.com/#narrow/stream/237662-VsCoq-devs-.26-users/topic/Cannot.20add.20monomorphic.20constraints/near/408931549

Collaborator Author

rtetley commented Jan 17, 2024

On first investigation there seems to be a strange behaviour in manual mode. To reproduce:

Interpret to the line in question (182). This should trigger the error.
Invalidate the state by making and edit, for example add a point after the first command, i.e Derive Signature for orec_graph.
Rewrite the normal line and step forward.
Now everything should work fine...

rtetley added the bug label

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment