test-suite/bugs/closed/HoTT_coq_048.v


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. *)