IIRC, the match it generates often ends up being a dependent match using the convoy pattern once nontrivial functions start being written, which quickly gets re

IIRC, the match it generates often ends up being a dependent match using the convoy pattern once nontrivial functions start being written, which quickly gets really really hard to read. Maybe this is partly the fault of Coq's matching requiring the convoy pattern (unlike Agda's or Idris's), but I find it extremely difficult to read these terms, versus hand-written ones.