diff options
author | 2017-12-01 10:11:41 +0100 | |
---|---|---|
committer | 2017-12-01 10:16:49 +0100 | |
commit | 20c98eab851210702b39e1c66e005acfc351d8dd (patch) | |
tree | 957aab7aadfda8c10f251ff9d83f3f5b05c07dc5 /test-suite/bugs/closed/4390.v | |
parent | 0048cbe810c82a775558c14cd7fcae644e205c51 (diff) |
Proper nametab handling of global universe names
They are now bound at the library + module level and can be qualified
and shadowed according to the usual rules of qualified names.
Parsing and printing of universes "u+n" done as well.
In sections, global universes are discharged as well, checking that
they can be defined globally when they are introduced
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. |