From df6bb883920e3a03044d09f10b57a44a2e7c5196 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 10 Feb 2016 17:59:14 +0100
Subject: 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
---
 stm/stm.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index 5ad1aead61..56dcda6a4a 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))
-- 
cgit v1.2.3