From 1a519fc37e703b014e3bcc77de01edd82aabea5f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 25 Mar 2015 09:44:12 +0100
Subject: Another example about the consequence of a wrong computation of the
 number of recursively uniform parameters in the presence of let-ins.

In practice, more recursively non-uniform parameters were assumed and
this was used especially for checking positivity of nested types,
leading to refusing more nested types than necessary (see Inductive.v).
---
 test-suite/success/Inductive.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index de18ed96ef..0a4ae68733 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -144,3 +144,14 @@ Inductive IND5 (A : Type) (T := A) : Type := CONS5 : IND5 ((fun _ => A) 0) -> IN
    uniform parameters in the presence of let-ins (see #3491) *)
 
 Inductive IND6 (A:Type) (T:=A) := CONS6 : IND6 T -> IND6 A.
+
+(* An example of nested positivity which was rejected by the kernel
+   before 24 March 2015 (even with Unset Elimination Schemes to avoid
+   the _rect bug) due to the wrong computation of non-recursively
+   uniform parameters in list' *)
+
+Inductive list' (A:Type) (B:=A) :=
+| nil' : list' A
+| cons' : A -> list' B -> list' A.
+
+Inductive tree := node : list' tree -> tree.
-- 
cgit v1.2.3