[ new ] Added new --exact-split option and CATCHALL pragma.
  The --exact-split flag causes Agda to raise an error whenever
  a clause in a definition by pattern matching cannot be made to
  hold definitionally (i.e. as a reduction rule). Specific clauses
  can be excluded from this check by means of the {-# CATCHALL #-}
  pragma.