From ca630605330828b9b6456477b0fd4f8a0c3f1831 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 21 May 2017 22:23:24 +0200
Subject: 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.
---
 test-suite/success/Record.v | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'test-suite')

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 }.
-- 
cgit v1.2.3