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.

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

Missing abstraction of const_relevance for opaques (Anomaly "File "kernel/cClosure.ml", line 138, characters 6-12: Assertion failed.") #18594

Closed
SkySkimmer opened this issue Jan 31, 2024 · 0 comments · Fixed by #18596
Closed

Missing abstraction of const_relevance for opaques (Anomaly "File "kernel/cClosure.ml", line 138, characters 6-12: Assertion failed.") #18594

SkySkimmer opened this issue Jan 31, 2024 · 0 comments · Fixed by #18596
Milestone
8.19.1

Comments

@SkySkimmer
Copy link
Contributor 

Set Universe Polymorphism.

Lemma foo@{s| |} (A:Type@{s|Set}) (a:A) : A.
Proof.
  exact a.
Qed.

Definition bar : foo nat = foo (id nat) := eq_refl.
@SkySkimmer SkySkimmer mentioned this issue Jan 31, 2024
Open
SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Jan 31, 2024
@SkySkimmer
Fix universe abstraction for const_relevance of opaques
9badbc2 
Fix coq#18594
@SkySkimmer SkySkimmer mentioned this issue Jan 31, 2024
Merged
SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Jan 31, 2024
@SkySkimmer
Fix universe abstraction for const_relevance of opaques
274cf97 
Fix coq#18594
@coqbot-app coqbot-app bot added this to the 8.19.1 milestone Feb 5, 2024
SkySkimmer added a commit that referenced this issue Feb 5, 2024
@SkySkimmer
Fix universe abstraction for const_relevance of opaques
c43d5ca 
Fix #18594

(cherry picked from commit 274cf97)
@SkySkimmer SkySkimmer mentioned this issue Feb 6, 2024
Closed
louiseddp pushed a commit to louiseddp/coq that referenced this issue Feb 27, 2024
@SkySkimmer @louiseddp
Fix universe abstraction for const_relevance of opaques
fe366cd 
Fix coq#18594
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
8.19.1
Development

Successfully merging a pull request may close this issue.

Fix universe abstraction for const_relevance of opaques SkySkimmer/coq
1 participant
@SkySkimmer