Remove special case for implicit inductive parameters

Co-authored-by: Jasper Hugunin <jasper@hugunin.net>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>

4 files changed, 22 insertions, 2 deletions

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_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) }.
diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out
index ff2556c5dc..e6c2806433 100644
--- a/test-suite/output/Inductive.out
+++ b/test-suite/output/Inductive.out
@@ -1,6 +1,10 @@
 The command has indeed failed with message:
-Last occurrence of "list'" must have "A" as 1st argument in
- "A -> list' A -> list' (A * A)%type".
+In environment
+list' : Set -> Set
+A : Set
+a : A
+l : list' A
+Unable to unify "list' (A * A)%type" with "list' A".
 Inductive foo (A : Type) (x : A) (y : A := x) : Prop :=  Foo : foo A x
 
 Arguments foo _%type_scope
diff --git a/test-suite/success/InductiveVsImplicitsVsTC.v b/test-suite/success/InductiveVsImplicitsVsTC.v
new file mode 100644
index 0000000000..9b787867fc
--- /dev/null
+++ b/test-suite/success/InductiveVsImplicitsVsTC.v
@@ -0,0 +1,10 @@
+Class C := {}.
+
+Definition useC {c:C} := nat.
+
+Inductive foo {a b : C} := CC : useC -> foo.
+(* If TC search runs before parameter unification it will pick the
+   wrong instance for the first parameter.
+
+   useC makes sure we don't completely skip TC search.
+*)