From 64401334b9707f74b9e9fedfed64f10c5e7a01b9 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 21 Nov 2001 12:29:21 +0000
Subject: La synthèse des '?' dans l'exemple avec un let était un peu trop
 ambitieuse...

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

diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 13814d9d80..f17fecc1e2 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -12,8 +12,19 @@ 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).
+Definition c [A;Q:(nat*A->Prop)->Prop;P] :=
+   (Q [p:nat*A]let (i,v) = p in (P i v)).
 
+(* What does this test ? *)
 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
+ (fold_right ([a][r]if (p a) then r else false) true l).
+
+(* Checks that solvable ? in the lambda prefix of the definition are harmless*)
+Parameter A1,A2,F,B,C : Set.
+Parameter f : F -> A1 -> B.
+Definition f1 [frm0,a1]: B := (f frm0 a1).
+
+(* Checks that solvable ? in the type part of the definition are harmless *)
+Definition f2 : (frm0:?;a1:?)B := [frm0,a1](f frm0 a1).
+
-- 
cgit v1.2.3