diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-02-10 17:59:14 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-02-10 17:59:14 +0100 |
| commit | df6bb883920e3a03044d09f10b57a44a2e7c5196 (patch) | |
| tree | a7b6f7bf90827f9adc4bd8159031f65d18660b6b /stm/stm.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 'stm/stm.ml')
| -rw-r--r-- | stm/stm.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 5ad1aead6..56dcda6a4 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -513,7 +513,10 @@ end = struct (* {{{ *) let rec fill id = if (get_info id).state = None then fill (Vcs_aux.visit v id).next else copy_info_w_state v id in - fill stop + let v = fill stop in + (* We put in the new dag the first state (since Qed shall run on it, + * see check_task_aux) *) + copy_info_w_state v start let nodes_in_slice ~start ~stop = List.rev (List.map fst (nodes_in_slice ~start ~stop)) |