Include review suggestions

1 files changed, 23 insertions, 7 deletions

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.