aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4390.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed/4390.v')
-rw-r--r--test-suite/bugs/closed/4390.v6
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.