diff options
| author | Emilio Jesus Gallego Arias | 2019-08-24 02:36:52 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-10-07 10:36:37 +0200 |
| commit | ebe43dddd50b96c8553e1fbdf3d26413eac47806 (patch) | |
| tree | 4f8a2a459fb90f68c434d75ae032bd797c7c6756 /dev | |
| parent | ef7cade43d514cb8f3d6022c298fdc467fcc4a33 (diff) | |
[vernac] Split vernacular translation and interpretation.
This allows UI clients to implement a different state management
strategy with regards to proofs, and in particular to override
`Vernacinterp.interp`.
This is work in progress towards having a true `VtTactic` which shall
not perform any state changes non-functionally, and actually removing
the series of `assert false` due to meta-vernacs.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions