aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-10-02 23:48:23 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-10-02 23:57:22 +0200
commita0e47bcf277d11ec7d2272bc5167fee898ad9016 (patch)
treee4323e150457f947400cd26c84ef294f33c1da97 /test-suite
parent0c320e79ba30bf567d4ca194bc114d733baf76e5 (diff)
Implement module subtyping for polymorphic constants (errors on
inductives). The implementation constant should have the a universe instance of the same length, we assume the universes are in the same order and we check that the definition does not add any constraints to the expected ones. This fixes bug #3670.
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/3670.v23
1 files changed, 23 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3670.v b/test-suite/bugs/closed/3670.v
new file mode 100644
index 000000000..c0f03261a
--- /dev/null
+++ b/test-suite/bugs/closed/3670.v
@@ -0,0 +1,23 @@
+Set Universe Polymorphism.
+Module Type FOO.
+ Parameter f : Type -> Type.
+ Parameter h : forall T, f T.
+End FOO.
+
+Module Type BAR.
+ Include FOO.
+End BAR.
+
+Module Type BAZ.
+ Include FOO.
+End BAZ.
+
+Module BAR_FROM_BAZ (baz : BAZ) <: BAR.
+
+ Definition f : Type -> Type.
+ Proof. exact baz.f. Defined.
+
+ Definition h : forall T, f T.
+ Admitted.
+
+Fail End BAR_FROM_BAZ.