5 files changed, 13 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_010.v b/test-suite/bugs/closed/HoTT_coq_010.v
index 42b1244fb5..caa7373f5e 100644
--- a/test-suite/bugs/closed/HoTT_coq_010.v
+++ b/test-suite/bugs/closed/HoTT_coq_010.v
@@ -1,3 +1,3 @@
-SearchAbout and.
+Search and.
 (* Anomaly: Mismatched instance and context when building universe substitution.
 Please report. *)
diff --git a/test-suite/bugs/closed/bug_11585.v b/test-suite/bugs/closed/bug_11585.v
new file mode 100644
index 0000000000..6294668323
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11585.v
@@ -0,0 +1,3 @@
+Fail Inductive type {type : Type} : Type := T : type.
+
+Inductive type {type : Type} : Type := T .
diff --git a/test-suite/bugs/closed/bug_11941.v b/test-suite/bugs/closed/bug_11941.v
new file mode 100644
index 0000000000..87cb462991
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11941.v
@@ -0,0 +1,5 @@
+Inductive Box A := box (_:A).
+Inductive unit := tt.
+Definition t := unit.
+Record foo := { bar : Box t }.
+Fail Scheme Equality for foo.
diff --git a/test-suite/bugs/closed/bug_3900.v b/test-suite/bugs/closed/bug_3900.v
index 6be2161c2f..ddede74acc 100644
--- a/test-suite/bugs/closed/bug_3900.v
+++ b/test-suite/bugs/closed/bug_3900.v
@@ -9,5 +9,5 @@ Variable Pmor : forall s d : obj, morphism A (projT1 s) (projT1 d) -> Type.
 Class Foo (x : Type) := { _ : forall y, y }.
 Local Instance ishset_pmor {s d m} : Foo (Pmor s d m).
 Proof.
-SearchAbout ((forall _ _, _) -> Foo _).
+Search ((forall _ _, _) -> Foo _).
 Abort.
diff --git a/test-suite/bugs/closed/bug_5233.v b/test-suite/bugs/closed/bug_5233.v
index 06286c740d..63e33b63f7 100644
--- a/test-suite/bugs/closed/bug_5233.v
+++ b/test-suite/bugs/closed/bug_5233.v
@@ -1,2 +1,5 @@
 (* Implicit arguments on type were missing for recursive records *)
 Inductive foo {A : Type} : Type := { Foo : foo }.
+
+(* Implicit arguments can be overidden *)
+Inductive bar {A : Type} : Type := { Bar : @bar (A*A) }.