diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-05 12:56:11 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-05 12:56:11 +0100 |
| commit | 2c5e81e3bc6ec17d253aeedd1b2bf4ccd3b81933 (patch) | |
| tree | 1e8d3db28d8d19b575e9e555f6ce379960c842c1 /test-suite/bugs/closed/4390.v | |
| parent | d403b2200ef32afd1eb1087a1f0ef2e6b8bb93f6 (diff) | |
| parent | 17b620f8bdf47a744d24513dcaef720d9160d443 (diff) | |
Merge PR #890: Global universe declarations
Diffstat (limited to 'test-suite/bugs/closed/4390.v')
| -rw-r--r-- | test-suite/bugs/closed/4390.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/bugs/closed/4390.v b/test-suite/bugs/closed/4390.v index a96a13700..c069b2d9d 100644 --- a/test-suite/bugs/closed/4390.v +++ b/test-suite/bugs/closed/4390.v @@ -8,16 +8,16 @@ Universe i. End foo. End M. -Check Type@{i}. +Check Type@{M.i}. (* Succeeds *) Fail Check Type@{j}. (* Error: Undeclared universe: j *) -Definition foo@{j} : Type@{i} := Type@{j}. +Definition foo@{j} : Type@{M.i} := Type@{j}. (* ok *) End A. - +Import A. Import M. Set Universe Polymorphism. Fail Universes j. Monomorphic Universe j. |