Allow “!” to start a larger operator

This causes it to be usable for a bang binding only if not directly followed by
additional operator chars, which should be the norm when intended as a bang
binding.
Add regression test for operators starting with "!"
Improve quasiquote patterns for MN

In the past, this elaborated to `_`.  However, this led to pattern matches
confusing built-in types like `()`, as these are named with `MN`. This
update makes the generated pattern more specific.
Merge pull request #1440 from Melvar/fix-bangbind-op

Allow “!” to start a larger operator
Merge pull request #1444 from david-christiansen/reflection-updates

Improve quasiquote patterns for MN
Split elaborator into multiple source files
Merge branch 'master' of github.com:idris-lang/Idris-dev
Update version number
Add %no_implicit directive

'implicit' is useful, but can cause problems when there are lots of
places implicit coercions can be applied. In particular, in Effects,
'lift' can be applied to each operation, and to the combination of
operations in >>=, so if there's an error the elaborator will try an
exponentially increasing number of things depending on the number of
>>=s.

This is a bit of an ugly hack, but it allows certain definitions (such
as >>=) to be non-coercible, so this exponential explosion doesn't
happen any more.

Fixes #1446
Bump upper bound on parsers dependency
Merge pull request #1447 from jwiegley/master

Bump upper bound on parsers dependency
Don't show irrelevant MNs in prover

Previously, proof steps like applyTactic would introduce MNs to the
proof state, with names like {scriptVar231}. This change hides those, as
the user cannot type them anyway.

If they are used in a later assumption, then they will be shown anyway.
Lift out proof term into a separate module

This should make it easier to experiment with alternative (hopefully
more efficient) representations
Merge branch 'master' of github.com:idris-lang/Idris-dev
Merge pull request #1450 from david-christiansen/dont-show-mn-in-proof

Don't show irrelevant MNs in prover
Use a zipper-like proof state

Proof state now contains the term in focus, its environment, and a path
through the complete term to reach that sub-term. As a result, large
proof terms are now checked more quickly

Cleaned up a couple of other things on the way...
Merge branch 'master' of github.com:idris-lang/Idris-dev
Search subterm for goal first
Save some allocations in updateSolved

Traverse the term to see if any holes need updated. The extra traversal
appears to be worth it, to save allocations when no updates are needed.