|
|
We make the vernacular implementation self-contained in the `vernac/`
directory. To this extent we relocate the parser, printer, and AST to
the `vernac/` directory, and move a couple of hint-related types to
`Hints`, where they do indeed belong.
IMO this makes the code easier to understand, and provides a better
modularity of the codebase as now all things under `tactics` have 0
knowledge about vernaculars.
The vernacular extension machinery has also been moved to `vernac/`,
this will help when #6171 [proof state cleanup] is completed along
with a stronger typing for vernacular interpretation that can
distinguish different types of effects vernacular commands can perform.
This PR introduces some very minor source-level incompatibilities due
to a different module layering [thus deprecating is not
possible]. Impact should be relatively minor.
|
Emilio Jesus Gallego Arias
Armaël Guéneau