From 1dd8d826592507046b35128800578149021dab4c Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 2 May 2016 17:11:22 +0200
Subject: Fix for #4603, part 3: definitions inside proofs not handled properly
 by coqc.

Patch by Matthieu, Enrico and myself.
---
 stm/stm.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index bec9d18d51..95cecb7fe2 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1839,7 +1839,7 @@ let known_state ?(redefine_qed=false) ~cache id =
             if ctac then Hooks.(call tactic_being_run true); 
             vernac_interp id x;
             if ctac then Hooks.(call tactic_being_run false); 
-	    if eff then update_global_env ()), cache, true
+	    if eff then update_global_env ()), (if eff then `Yes else cache), true
       | `Fork ((x,_,_,_), None) -> (fun () ->
             reach view.next; vernac_interp id x;
             wall_clock_last_fork := Unix.gettimeofday ()
@@ -2247,13 +2247,14 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
           vernac_interp (VCS.get_branch_pos head) x; `Ok
 
       | VtSideff l, w ->
+	  let ceff_in_proof = not (VCS.Branch.equal head VCS.Branch.master) in
           let id = VCS.new_node ~id:newtip () in
           VCS.checkout VCS.Branch.master;
-          VCS.commit id (Cmd {ctac=false;ceff=true;cast=x;cids=l;cqueue=`MainQueue});
 	  let replay = match x.expr with
 	    | VernacDefinition(_, _, DefineBody _) -> None
 	    | _ -> Some x
 	  in
+          VCS.commit id (Cmd {ctac=false;ceff=ceff_in_proof;cast=x;cids=l;cqueue=`MainQueue});
 	  VCS.propagate_sideff replay;
           VCS.checkout_shallowest_proof_branch ();
           Backtrack.record (); if w == VtNow then finish (); `Ok
-- 
cgit v1.2.3