Add a specification of a CFG parser-recognizer
WIP non-computational parser

Also, a [clear abstract] tactic based on typeclasses that clears the
environment of useless things.  It's currently slow, because it'll run
[abstract] and typecheck the proof term for every hypothesis it
clears.  But I suspect this can be fixed by being smarter about
occurs-checking and such.

The parser can currently parse items, and I've started work on having
it parse patterns.