Always accept antiquotations

[Kha]

There was some confusion about incQuotDepth on Zulip, which is unfortunate since the combinator really only exists for bootstrapping. This PR simplifies the code so that antiquotations are accepted everywhere (but still need a corresponding transformer/elaborator to actually do something). The performance impact should be offset by fast checks for the happy (non-quotation) path.

[Kha]

!bench

[Kha]

but still need a corresponding transformer/elaborator to actually do something

This PR does not yet add an elaborator for antiquotations on the top level (command and term cats), but that would definitely be possible. It would enable a Template Haskell-like approach to metaprogramming where you invoke the metaprogram using a direct, statically typed function call instead of a macro using arbitrary syntax for its parameters. Not sure if anyone has missed something like this so far (/cc @gebner @digama0?)

[leanprover-bot]

Here are the benchmark results for commit 94fb610.
There were no significant changes.