aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorEnrico Tassi2014-12-27 20:43:07 +0100
committerEnrico Tassi2014-12-27 20:43:07 +0100
commitaeb5daa2efdb2d0f2c75670e11d409f24528c54a (patch)
tree3860b2abe9c0eda0077149fe11b4fa885d24d342 /dev
parent1801eab1c6685f3d1a0311ac1074f252efcccbc5 (diff)
STM: check with the kernel proof terms on the worker too
Before this commit the worker was sending back a proof term as built by tactics. The master receives the proof terms and eventually (when one clicks on the gears in CoqIDE) check it with the kernel. This meant that errors like the ones produced by the "fix" tactics were discovered very late. Now a worker checks with its kernel the proof term before sending it back. The term is also checked by the master, eventually, but the error is signaled early.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions