diff options
| author | Enrico Tassi | 2014-12-27 20:43:07 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-12-27 20:43:07 +0100 |
| commit | aeb5daa2efdb2d0f2c75670e11d409f24528c54a (patch) | |
| tree | 3860b2abe9c0eda0077149fe11b4fa885d24d342 /dev | |
| parent | 1801eab1c6685f3d1a0311ac1074f252efcccbc5 (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
