Navigation Menu

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

Jump to bottom

Universe conflict when attempting to rewrite with a certain equivalence #5521

Closed
coqbot opened this issue May 13, 2017 · 3 comments · Fixed by #14137
Closed

Universe conflict when attempting to rewrite with a certain equivalence #5521

coqbot opened this issue May 13, 2017 · 3 comments · Fixed by #14137
Labels
part: tactics
Milestone
8.16+rc1

Comments

@coqbot
Copy link
Contributor

coqbot commented May 13, 2017

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#5521
From: @jwiegley
Reported version: 8.6
CC: @JasonGross, @bmsherman

See also: BZ#4806
See also: BZ#5384
@coqbot
Copy link
Contributor Author

coqbot commented May 13, 2017

Comment author: @jwiegley

The attached gives an error when trying to rewrite on the last line; but if you
comment out the two lines indicated in my comment, it works. Why would
universes be conflicting with those two lines?

@coqbot
Copy link
Contributor Author

coqbot commented May 13, 2017

Comment author: @jwiegley

Created attachment 843
Bug.v

Attached file: Bug.v (text/plain, 2293 bytes)
Description: Bug.v

@coqbot
Copy link
Contributor Author

coqbot commented May 17, 2017

Comment author: @bmsherman

Note that this is specifically a bug for rewriting in Type.

See also:
bug BZ#4806
bug BZ#5384

@coqbot coqbot mentioned this issue Mar 30, 2018
Closed
Alizter added a commit to mattam82/coq that referenced this issue Jan 4, 2022
@Alizter
Updated bugs in test-suite and more testing of generalized rewriting.
c592cec 
Added coq#4632 coq#5384 coq#5521 coq#6278 coq#8739 coq#11011 coq#12240 coq#15279 to test-suite.
@Alizter Alizter mentioned this issue Jan 4, 2022
Merged
4 tasks
Alizter added a commit to mattam82/coq that referenced this issue Jan 4, 2022
@Alizter
Updated bugs in test-suite and more testing of generalized rewriting.
6889400 
Added coq#4632 coq#5384 coq#5521 coq#6278 coq#7675 coq#8739 coq#11011 coq#12240 coq#15279 to
test-suite.
Alizter added a commit to mattam82/coq that referenced this issue Jan 4, 2022
@Alizter
Updated bugs in test-suite and more testing of generalized rewriting.
3932873 
Added coq#4632 coq#5384 coq#5521 coq#6278 coq#7675 coq#8739 coq#11011 coq#12240 coq#15279 to
test-suite.
Alizter added a commit to mattam82/coq that referenced this issue Jan 5, 2022
@Alizter
Updated bugs in test-suite and more testing of generalized rewriting.
0859f98 
Added coq#4632 coq#5384 coq#5521 coq#6278 coq#7675 coq#8739 coq#11011 coq#12240 coq#15279 to
test-suite.
@Zimmi48 Zimmi48 added this to the 8.16+rc1 milestone Jul 4, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
part: tactics
Projects
None yet
Milestone
8.16+rc1
Development

Successfully merging a pull request may close this issue.

Improve generalized rewriting in Type and with univpoly mattam82/coq
2 participants
@Zimmi48 @coqbot