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

trunk-polyproj seems to be missing eta for records? (polyproj) #104

Closed

JasonGross opened this issue Apr 8, 2014 · 1 comment

JasonGross commented Apr 8, 2014

Set Implicit Arguments.

Require Import Logic.

Global Set Universe Polymorphism.
Global Set Asymmetric Patterns.
Local Set Record Elimination Schemes.
Local Set Primitive Projections.

Record prod (A B : Type) : Type :=
  pair { fst : A; snd : B }.

Check fun x : prod Set Set => eq_refl : x = pair (fst x) (snd x).

fails. Has eta for records been removed from trunk-polyproj? Is it still slated for 8.5?

Author

JasonGross commented May 2, 2014

Oops, I re-reported a more accurate version as #124. Closing this one.

JasonGross closed this as completed

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