More precise on preventing clash between bound vars name and hidden impargs.

We want to avoid capture in "Inductive I {A} := C : forall A, I".
But in "Record I {A} := { C : forall A, A }.", non recursivity ensures
that no clash will occur.

This fixes previous commit, with which it could possibly be merged.

1 files changed, 5 insertions, 0 deletions

diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v
index 8334322c99..6f27c1d369 100644
--- a/test-suite/success/Record.v
+++ b/test-suite/success/Record.v
@@ -87,3 +87,8 @@ Record R : Type := {
   P (A : Type) : Prop := exists x : A -> A, x = x;
   Q A : P A -> P A
 }.
+
+(* We allow reusing an implicit parameter named in non-recursive types *)
+(* This is used in a couple of development such as UniMatch *)
+
+Record S {A:Type} := { a : A; b : forall A:Type, A }.