From a0e47bcf277d11ec7d2272bc5167fee898ad9016 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 2 Oct 2014 23:48:23 +0200 Subject: 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. --- test-suite/bugs/closed/3670.v | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 test-suite/bugs/closed/3670.v (limited to 'test-suite') 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. -- cgit v1.2.3