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

(limited to 'test-suite')

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