From 7d170e8e2ee9bc08bfb05f623190a51680410a37 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 20 Jan 2006 17:00:38 +0000
Subject: Test bug 983

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7901 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/Inductive.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 33da5e4cee..1adcbd39a1 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -42,3 +42,11 @@ Inductive Finite (A : Set) : LList A -> Prop :=
   | Finite_LNil : Finite LNil
   | Finite_LCons :
       forall (a : A) (l : LList A), Finite l -> Finite (LCons a l).
+
+(* Check positivity modulo reduction (cf bug #983) *)
+
+Record P:Type := {PA:Set; PB:Set}.
+
+Definition F (p:P) := (PA p) -> (PB p).
+
+Inductive I_F:Set := c : (F (Build_P nat I_F)) -> I_F.
-- 
cgit v1.2.3