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 +++++-
 test-suite/bugs/closed/4603.v | 10 ++++++++++
 2 files changed, 15 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/4603.v

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
 
diff --git a/test-suite/bugs/closed/4603.v b/test-suite/bugs/closed/4603.v
new file mode 100644
index 0000000000..e7567623a6
--- /dev/null
+++ b/test-suite/bugs/closed/4603.v
@@ -0,0 +1,10 @@
+Axiom A : Type.
+
+Goal True. exact I.
+Check (fun P => P A).
+Abort.
+
+Goal True.
+Definition foo (A : Type) : Prop:= True. 
+  set (x:=foo). split.
+Qed.
\ No newline at end of file
-- 
cgit v1.2.3