Ajout d'un exemple de Christine

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2365 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 10 insertions, 1 deletions

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.
+