aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3804.v
diff options
context:
space:
mode:
authorGravatar Xavier Clerc <xavier.clerc@inria.fr>2014-11-25 17:11:40 +0100
committerGravatar Xavier Clerc <xavier.clerc@inria.fr>2014-11-25 17:11:40 +0100
commitf839f718fc6271aeb014c9cb5abdf9106b1c26be (patch)
treed73a336ba7e8bc55628681b4486d91dc08673dd0 /test-suite/bugs/closed/3804.v
parentec9fda550cd997cc342e2f109cd6ceeadebec0e0 (diff)
Bug #3804 is actually closed (thanks to Jason Gross for the notification).
Diffstat (limited to 'test-suite/bugs/closed/3804.v')
-rw-r--r--test-suite/bugs/closed/3804.v12
1 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3804.v b/test-suite/bugs/closed/3804.v
new file mode 100644
index 000000000..da9290cba
--- /dev/null
+++ b/test-suite/bugs/closed/3804.v
@@ -0,0 +1,12 @@
+Set Universe Polymorphism.
+Module Foo.
+ Definition T : sigT (fun x => x).
+ Proof.
+ exists Set.
+ abstract exact nat.
+ Defined.
+End Foo.
+Module Bar.
+ Include Foo.
+End Bar.
+Definition foo := eq_refl : Foo.T = Bar.T.