STM: fix handling of side effects in vio2vo

3 files changed, 20 insertions, 2 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 392225480..d615dc170 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1148,6 +1148,11 @@ end = struct (* {{{ *)
     msg_info(
       str(Printf.sprintf "Checking task %d (%s%s) of %s" i r_name extra name));
     VCS.restore document;
+    let start =
+      let rec aux cur =
+        try aux (VCS.visit cur).next
+        with VCS.Expired -> cur in
+      aux stop in
     try
       Reach.known_state ~cache:`No stop;
       (* The original terminator, a hook, has not been saved in the .vio*)
@@ -1156,6 +1161,9 @@ end = struct (* {{{ *)
           (Lemmas.mk_hook (fun _ _ -> ())));
       let proof =
         Proof_global.close_proof ~keep_body_ucst_sepatate:true (fun x -> x) in
+      (* We jump at the beginning since the kernel handles side effects by also
+       * looking at the ones that happen to be present in the current env *)
+      Reach.known_state ~cache:`No start;
       vernac_interp stop ~proof
         { verbose = false; loc;
           expr = (VernacEndProof (Proved (true,None))) };
@@ -1190,7 +1198,7 @@ end = struct (* {{{ *)
     let bucket = (List.nth l i).Stateid.uuid in
     match check_task_aux (Printf.sprintf ", bucket %d" bucket) name l i with
     | None -> exit 1
-    | Some (po,pt) ->
+    | Some (po,_) ->
         let discharge c = List.fold_right Cooking.cook_constr d.(bucket) c in
         let con =
           Nametab.locate_constant
diff --git a/test-suite/Makefile b/test-suite/Makefile
index b2f8ad79d..4a3a287c0 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -435,7 +435,7 @@ vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v))
 	$(HIDE){ \
 	  $(bincoqc) -quick -R vio vio $* 2>&1 && \
 	  $(coqtop) -R vio vio -vio2vo $*.vio 2>&1 && \
-	  $(bincoqchk) -R vio vio $(subst /,.,$*) 2>&1; \
+	  $(bincoqchk) -R vio vio -norec $(subst /,.,$*) 2>&1; \
 	  if [ $$? = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
diff --git a/test-suite/vio/seff.v b/test-suite/vio/seff.v
new file mode 100644
index 000000000..447e77983
--- /dev/null
+++ b/test-suite/vio/seff.v
@@ -0,0 +1,10 @@
+Inductive equal T (x : T) : T -> Type := Equal : equal T x x.
+
+Module bla.
+
+Lemma test n : equal nat n (n + n) -> equal nat (n + n + n) n.
+Proof using.
+intro H. rewrite <- H. rewrite <- H. exact (Equal nat n).
+Qed.
+
+End bla.