Add tests for #13303

3 files changed, 40 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_13303.v b/test-suite/bugs/closed/bug_13303.v
new file mode 100644
index 0000000000..6bee24b48a
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13303.v
@@ -0,0 +1,27 @@
+Module Pt1.
+
+  Module M. Universe i. End M.
+  Module N. Universe i. End N.
+  Import M.
+  Notation foo := Type@{i (* M.i??? *)}.
+  Import N.
+  Fail Check foo : Type@{M.i}. (* should NOT succeed *)
+  Check foo : Type@{i (* N.i *)}. (* should succeed *)
+
+  Definition bar@{i} := Type@{i}.
+  Check bar : Type@{N.i}.
+  Check bar : Type@{M.i}.
+
+End Pt1.
+
+Module Pt2.
+
+  Module M. Universe i. Notation foo := Type@{i}. End M.
+
+  Definition foo1 := M.foo.
+  (* should succeed, currently errors undeclared universe i *)
+
+  Definition foo2@{i} : Type@{i} := M.foo.
+  (* should succeed, currently errors universe inconsistency *)
+
+End Pt2.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index aca7f0a1e1..0fbb4f4c11 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -159,6 +159,9 @@ Arguments axbar' _%type_scope
 Expands to: Constant UnivBinders.axbar'
 The command has indeed failed with message:
 When declaring multiple axioms in one command, only the first is allowed a universe binder (which will be shared by the whole block).
+foo@{i} = Type@{M.i} -> Type@{i}
+     : Type@{max(M.i+1,i+1)}
+(* i |=  *)
 bind_univs.mono = 
 Type@{bind_univs.mono.u}
      : Type@{bind_univs.mono.u+1}
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index c0db83d769..ed6e90b2a6 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -151,6 +151,16 @@ About axfoo. About axbar. About axfoo'. About axbar'.
 
 Fail Axiom failfoo failbar@{i} : Type.
 
+(* Notation interaction *)
+Module Notas.
+  Unset Universe Polymorphism.
+  Module Import M. Universe i. End M.
+
+  Polymorphic Definition foo@{i} := Type@{M.i} -> Type@{i}.
+  Print foo. (* must not print Type@{i} -> Type@{i} *)
+
+End Notas.
+
 (* Universe binders survive through compilation, sections and modules. *)
 Require TestSuite.bind_univs.
 Print bind_univs.mono.