Add tests for #13303

2 files changed, 13 insertions, 0 deletions

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.