From 927e88de465e94bf18b970b45faaf97b4c2dff82 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 12 Apr 2016 18:59:55 +0200
Subject: Quick fix for #4603 (part 2): Anomaly: Universe undefined

This is a follow-up on Matthieu's 7e7b5684

The Definition command was classified incorrectly when a body was provided.
This fix is a bit ad-hoc. A better one would require more expressiveness in
side effect classification, but I'll do it in trunk only since it could impact
plugins.

Thanks a lot to Enrico for his help!
---
 stm/stm.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index a6d119f0cd..094457431e 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2250,7 +2250,11 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
           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});
-          VCS.propagate_sideff (Some x);
+	  let replay = match x.expr with
+	    | VernacDefinition(_, _, DefineBody _) -> None
+	    | _ -> Some x
+	  in
+	  VCS.propagate_sideff replay;
           VCS.checkout_shallowest_proof_branch ();
           Backtrack.record (); if w == VtNow then finish (); `Ok
 
-- 
cgit v1.2.3