[ clarify ] Removed defacto identity substitution in BasicOps.give.

When meta instantiations became open terms in context (instead of
lambdas), it was not recognized that the application sequence
corresponds to the identity substitution.
https://github.com/agda/agda/commit/5e6ffac27d7f37dbe6d9701fcf0feff3d7431827
[ cosmetics ] and comments.
[ interaction ] Better error message when type checking given expr fails.
[ debug ] printing in Give and checkExpr QuestionMark.
[ Issue 1342 ] Fixed by outlawing with on module parameter.

The module free variables should stay free, so no with on them.
[ Issue 1342 ] Test cases that trigger the new error.
[ Issue 1342 ] CHANGELOG
Merge branch 'maint-2.4.2'
[ Issue 1344 ] Added test case.
[ whitespace ] Fixed whitespace in Issue1344.agda
[ Issue 1345 ] Add context telescope to unquoted clauses before reification.
Merge branch 'maint-2.4.2'
[ fix-agda-whitespace ] Ignore hidden files, e.g. .#Bla.hs.

These are created in emacs whenever a file is unsaved.
fix-agda-whitespace failed in the presence of such a file before.
[ mytags ] Ignores now with .#Bla.hs files.  (All hidden files.)
[ refactor ] pulled Rules.LHS.checkLHS to toplevel.

For cosmetic reasons:  excessive indentation and super long local
functions need to be avoided.
[ subterm ] Deleted failed test case (to be successful soon).
[ subterm ] new: Termination.Order.nonIncreasing
[ subterm ] Refactor: added TermDBP constructor to DeBruijnPat.
[ subterm ] New feature in termination checker: Recognize simple subterms in dot patterns.

This allows e.g. to see that .(suc (x + y)) is structurally bigger
than (x + y).
[ subterm ] Successful test for using subterms in Termination checker.