[ micro refactor ] in Pretty CallInfo.
Termination check failure is now a TypeError.

We no longer continue after termination check failures.
Use pragmas {-# NON_TERMINATING #-} and {-# NO_TERMINATION_CHECK #-}
if you want to do so.
[ CHANGELOG ] for termination failure is error.
[ testsuite ] Updated termination error messages.

All termination errors now come with a range.
Only the first termination error will be reported now.
Added some {-# NON_TERMINATING #-} pragmas to keep original
test case behavior.
Merge ../agda
[ factored out ] terminationErrorHighlighting
Special highlighting for termination errors (showing call sites).
Merge ../agda
[ tiny refactor ] Use gets with record projection!
[ clean ] Purged termErrs from state.

Since we are reporting a termination right away now, we do not need
the complicated information flow of termination errors anymore.
Merge ../agda
[ repair ] Highlighting termination errors should not erase previous
highlighting.

Unlike for other errors.
Merge ../agda
[ comment ] slightly clarified in Highlighting.Generate
[ factored ] out highlight_ from checkDeclaration monster
[ repair ] Do final highlighting before termination checking.

To get termination errors on top of highlighted code, not on
code with highlighting removed.
Merge ../agda
[ rename ] Import Syntax.Common as Common.
[ refactor ] Added Induction field to Internal.Con.

Constructors need to know whether they are inductive or coinductive,
e.g. for checking strictly rigid variable occurrences.
Also changed DCon to carry the ConHead instead of just QName.
[ issue 1271 ] test case