aboutsummaryrefslogtreecommitdiff
path: root/dev/doc
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 /dev/doc
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 'dev/doc')
0 files changed, 0 insertions, 0 deletions