[ Issue 1380 ] Fixed by keeping track of original dot patterns
in the translation of patterns to mpatterns.
[ Issue 1379 ] Fixed the range of with clauses starting with an ellipsis.
[ cosmetics ] Broke a too long line.
[ interaction ] Show also open instance metas.

Could not see any effect on the interaction test suite.
Merge branch 'maint-2.4.2'

Conflicts:
	src/full/Agda/Syntax/Concrete.hs
	src/full/Agda/Syntax/Concrete/Definitions.hs
[ clean ] Removed some old, commented out code.
[ optim ] Use raiseS in construction of substitution.
[ clarify ] Some rewriting of the code for with display form generation.
[ refactor ] Express patToTerms via numberPatVars.
[ Issue 1377 ] If instance argument cannot be filled in immediately, add constraint to do it later.
[ clean ] Removed some old, commented out code.
[ big refactor ] Added reason to NotBlocked and NeutralLevel.

We now distinguish not only reduction stuck on a meta, but also on
neutral terms, by virtue of underapplication, and missing or absurd
clauses.  See Syntax.Internal.NotBlocked.
[ refactor ] Use ifBlockedType in Agda.TypeChecking.Empty.
[ refactor ] Overloaded empty for Doc and TCM Doc.
[ comment ] Remark on future use of DefaultSignatures.
[ new ] Null instance for Simplification.
[ removed ] Monoid instance for Agda.TypeChecking.Patterns.Match.Match.
[ clean ] Removed commented out and unused code.
[ NotBlocked ] new reason MissingClauses.
[ NotBlocked ] Use stuckOn to propagate NotBlocked info.