blob: 831bb3fc40f78538a3de3dc4ee2facaf0f02ea30 (
plain)
1
2
3
4
5
6
7
|
(** This is not the issue of https://github.com/HoTT/coq/issues/48, but was mentioned there. *)
Record Foo :=
{
foo := 1;
bar : foo = foo
}.
(* Anomaly: lookup_projection: constant is not a projection. Please report. *)
|