diff options
Diffstat (limited to 'test-suite/failure')
| -rw-r--r-- | test-suite/failure/univ_include.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/test-suite/failure/univ_include.v b/test-suite/failure/univ_include.v index fd17457f0..4be70d888 100644 --- a/test-suite/failure/univ_include.v +++ b/test-suite/failure/univ_include.v @@ -17,13 +17,14 @@ Module G (E : MU). Include F E. Print Universes. (* U <= T *) End G. -Print Universes. (* constraint lost! *) +Print Universes. (* Check if constraint is lost *) Module Mt. - Definition t :=T. + Definition t := T. End Mt. -Module P := G Mt. +Module P := G Mt. (* should yield Universe inconsistency *) +(* ... otherwise the following command will show that T has type T! *) Eval cbv delta [P.elt Mt.t] in P.elt. |