From e3b51f8f1fb7249d3485ff7effa7df1a23c0282d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 16 Nov 2001 23:09:32 +0000
Subject: *** empty log message ***

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

diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 6d52ec4c64..13814d9d80 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -10,3 +10,10 @@ Variable list:Set -> Set.
 Variable cons:(T:Set) T -> (list T) -> (list T).
 Goal (n:(list nat)) (EX l| (EX x| (n = (cons ? x l)))).
 
+(* Examples provided by Eduardo Gimenez *)
+
+Definition c [A,P] := [p:nat*A]let (i,v) = p in (P i v).
+
+Require PolyList.
+Definition list_forall_bool  [A:Set][p:A->bool][l:(list A)] : bool := 
+ (fold_right ([a][r]if (p a) then r else false) true l).
\ No newline at end of file
-- 
cgit v1.2.3