diff options
| author | Enrico Tassi | 2016-02-10 17:59:14 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2016-02-10 17:59:14 +0100 |
| commit | df6bb883920e3a03044d09f10b57a44a2e7c5196 (patch) | |
| tree | a7b6f7bf90827f9adc4bd8159031f65d18660b6b /lib/system.ml | |
| parent | 22ab7fff908c259d6e433da246bebac519009905 (diff) | |
STM: always stock in vio files the first node (state) of a proof
It used not to be the case when the proof contains Sideff, since
the code was picking the last known state and not necessarily the
first one. Because of side effects the last known state could be
the one corresponding to the side effect (that was executed to, say,
change the parser). This is also related to bug #4530
Diffstat (limited to 'lib/system.ml')
0 files changed, 0 insertions, 0 deletions