From 7af730c8408f294ebe568240a3288f24a0959847 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 21 Dec 2001 16:13:44 +0000
Subject: Ajout d'un exemple de Christine

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

diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index 5f0067412c..bd74742857 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -1,9 +1,18 @@
 (* Implicit on section variables *)
-(* Example submitted by David Nowak *)
 
 Set Implicit Arguments.
+
+(* Example submitted by David Nowak *)
+
 Section Spec.
 Variable A:Set.
 Variable op : (A:Set)A->A->Set.
 Infix 6 "#" op.
 Check (x:A)(x # x).
+
+(* Example submitted by Christine *)
+Record stack : Type := {type : Set; elt : type; 
+                        empty : type -> bool; proof : (empty elt)=true }.
+
+Check (type:Set; elt:type; empty:(type->bool))(empty elt)=true->stack.
+
-- 
cgit v1.2.3