From 010d031cc016ee7d539e3a0ea486a54229f769f6 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Tue, 13 Mar 2001 15:17:56 +0000
Subject: Finite

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1458 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/test_extraction.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/contrib/extraction/test_extraction.v b/contrib/extraction/test_extraction.v
index dbf48ec851..22a2cb99a7 100644
--- a/contrib/extraction/test_extraction.v
+++ b/contrib/extraction/test_extraction.v
@@ -40,3 +40,14 @@ Extraction (id' Set nat).
 
 Extraction let t = nat in (id' Set t). (* 5904-5916: Assertion failed *)
 
+Definition Ensemble := [U:Type]U->Prop.
+
+Definition Empty_set := [U:Type][x:U]False.
+
+Definition Add := [U:Type][A:(Ensemble U)][x:U][y:U](A y) \/ x==y.
+
+Inductive Finite [U:Type] : (Ensemble U) -> Set :=
+      Empty_is_finite: (Finite U (Empty_set U))
+   |  Union_is_finite:
+      (A: (Ensemble U)) (Finite U A) -> 
+      (x: U) ~ (A x) -> (Finite U (Add U A x)).
-- 
cgit v1.2.3