5 files changed, 22 insertions, 1 deletions
diff --git a/test-suite/bugs/2428.v b/test-suite/bugs/closed/2428.v
index a4f587a58d..b398a76d91 100644
--- a/test-suite/bugs/2428.v
+++ b/test-suite/bugs/closed/2428.v
@@ -5,6 +5,6 @@ Definition myFact := forall x, P x.
 Hint Extern 1 (P _) => progress (unfold myFact in *).
 
 Lemma test : (True -> myFact) -> P 3.
-Proof. 
+Proof.
   intros. debug eauto.
 Qed.
diff --git a/test-suite/bugs/4623.v b/test-suite/bugs/closed/4623.v
index 7ecfd98b67..7ecfd98b67 100644
--- a/test-suite/bugs/4623.v
+++ b/test-suite/bugs/closed/4623.v
diff --git a/test-suite/bugs/4624.v b/test-suite/bugs/closed/4624.v
index f5ce981cd0..f5ce981cd0 100644
--- a/test-suite/bugs/4624.v
+++ b/test-suite/bugs/closed/4624.v
diff --git a/test-suite/bugs/7333.v b/test-suite/bugs/closed/7333.v
index fba5b9029d..fba5b9029d 100644
--- a/test-suite/bugs/7333.v
+++ b/test-suite/bugs/closed/7333.v
diff --git a/test-suite/bugs/closed/7754.v b/test-suite/bugs/closed/7754.v
new file mode 100644
index 0000000000..229df93773
--- /dev/null
+++ b/test-suite/bugs/closed/7754.v
@@ -0,0 +1,21 @@
+
+Set Universe Polymorphism.
+
+Module OK.
+
+  Inductive one@{i j} : Type@{i} :=
+  with two : Type@{j} := .
+  Check one@{Set Type} : Set.
+  Fail Check two@{Set Type} : Set.
+
+End OK.
+
+Module Bad.
+
+  Fail Inductive one :=
+    with two@{i +} : Type@{i} := .
+
+  Fail Inductive one@{i +} :=
+    with two@{i +} := .
+
+End Bad.