Unable to build a covering for records containing definitions

[jakobbotsch]

Equations fails to build a covering for the following:

Record test := mk { foo : nat; bar := foo }.
Equations baz (t : test) : nat :=
baz (mk 0) := 0;
baz (mk (S n)) with true := {
  | true => 0;
  | false => 0
  }.

If bar := foo is removed it works.

[mattam82]

Hmm, that one's not so easy, it will take some time to get right.