aboutsummaryrefslogtreecommitdiff
path: root/tools/TimeFileMaker.py
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-06-07 15:22:31 +0200
committerEmilio Jesus Gallego Arias2019-06-26 12:27:04 +0200
commitd4aeb1ef92a9fc35b242a0d91488de60c24d7bbb (patch)
tree0c4165866165937fae20b0dfe9a334e55ea3b8b8 /tools/TimeFileMaker.py
parent2c39a12f5a8d7178b991595324692c1596ea9199 (diff)
[stm] [vernac] Remove special ?proof parameter from vernac main path
We move special vernac-qed handling to a special function, making the regular vernacular interpretation path uniform. This is an important step as it paves the way up to export the vernac DSL to clients, as there are no special vernacs anymore in the regular interp path, except for Load, which should be handled separately due to silly reasons, as morally it is a `VtNoProof` command.
Diffstat (limited to 'tools/TimeFileMaker.py')
0 files changed, 0 insertions, 0 deletions