1 files changed, 24 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3825.v b/test-suite/bugs/closed/3825.v
new file mode 100644
index 00000000..666c6463
--- /dev/null
+++ b/test-suite/bugs/closed/3825.v
@@ -0,0 +1,24 @@
+Set Universe Polymorphism.
+Set Printing Universes.
+
+Axiom foo@{i j} : Type@{i} -> Type@{j}.
+
+Notation bar := foo.
+
+Monomorphic Universes i j.
+
+Check bar@{i j}.
+Fail Check bar@{i}.
+
+Notation qux := (nat -> nat).
+
+Fail Check qux@{i}.
+
+Axiom TruncType@{i} : nat -> Type@{i}.
+
+Notation "n -Type" := (TruncType n) (at level 1) : type_scope.
+Notation hProp := (0)-Type.
+
+Check hProp.
+Check hProp@{i}.
+