summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/5011.v
blob: c3043ca5d125d283d0734c512070ac6299d20467 (plain)
1
2
Record decoder (n : nat) W := { decode : W -> nat }.
Existing Class decoder.