6 files changed, 25 insertions, 4 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.
diff --git a/test-suite/success/ROmega4.v b/test-suite/success/ROmega4.v
index 58ae5b8fb8..a724592749 100644
--- a/test-suite/success/ROmega4.v
+++ b/test-suite/success/ROmega4.v
@@ -3,12 +3,12 @@
     See also #148 for the corresponding improvement in Omega.
 *)
 
-Require Import ZArith ROmega.
+Require Import ZArith Lia.
 Open Scope Z.
 
 Goal let x := 3 in x = 3.
 intros.
-romega.
+lia.
 Qed.
 
 (** Example seen in #4132
@@ -22,5 +22,5 @@ Lemma foo
   (H : - zxy' <= zxy)
   (H' : zxy' <= x') : - b <= zxy.
 Proof.
-romega.
+lia.
 Qed.