Include review suggestions

3 files changed, 37 insertions, 11 deletions

diff --git a/doc/changelog/02-specification-language/11579-inductive-params.rst b/doc/changelog/02-specification-language/11579-inductive-params.rst
index 75358ab4ad..28bc8e9592 100644
--- a/doc/changelog/02-specification-language/11579-inductive-params.rst
+++ b/doc/changelog/02-specification-language/11579-inductive-params.rst
@@ -1,4 +1,7 @@
-- **Changed:**
-  Treatment of implicit inductive parameters in inductive declarations is less adhoc.
-  (`#11579 <https://github.com/coq/coq/pull/11579>`_,
-  by Maxime Dénès, Gaëtan Gilbert and Jasper Hugunin).
+- **Fixed:**
+  More robust and expressive treatment of implicit inductive
+  parameters in inductive declarations (`#11579
+  <https://github.com/coq/coq/pull/11579>`_, by Maxime Dénès, Gaëtan
+  Gilbert and Jasper Hugunin; fixes `#7253
+  <https://github.com/coq/coq/pull/7253>`_ and `#11585
+  <https://github.com/coq/coq/pull/11585>`_)
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 3396c5a0e7..8be7b1477b 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -45,6 +45,13 @@ type typing_constraint =
   | WithoutTypeConstraint (** A term of unknown expected type *)
 
 type use_typeclasses = NoUseTC | UseTCForConv | UseTC
+(** Typeclasses are used in 2 ways:
+
+- through the "Typeclass Resolution For Conversion" option, if a
+  conversion problem fails we try again after resolving typeclasses
+  (UseTCForConv and UseTC)
+- after pretyping we resolve typeclasses (UseTC) (in [solve_remaining_evars])
+*)
 
 type inference_flags = {
   use_typeclasses : use_typeclasses;
diff --git a/test-suite/success/InductiveVsImplicitsVsTC.v b/test-suite/success/InductiveVsImplicitsVsTC.v
index 9b787867fc..a98de32b70 100644
--- a/test-suite/success/InductiveVsImplicitsVsTC.v
+++ b/test-suite/success/InductiveVsImplicitsVsTC.v
@@ -1,10 +1,26 @@
-Class C := {}.
+Module NoConv.
+  Class C := {}.
 
-Definition useC {c:C} := nat.
+  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.
+  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.
-*)
+     useC makes sure we don't completely skip TC search.
+   *)
+End NoConv.
+
+Module ForConv.
+
+  Class Bla := { bla : Type }.
+
+  Instance bli : Bla := { bla := nat }.
+
+  Inductive vs := C : forall x : bla, x = 2 -> vs.
+  (* here we need to resolve TC to pass the conversion problem if we
+     combined with the previous example it would fail as TC resolution
+     for conversion is unrestricted and so would resolve the
+     conclusion too early. *)
+
+End ForConv.