diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-21 12:29:21 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-21 12:29:21 +0000 |
| commit | 64401334b9707f74b9e9fedfed64f10c5e7a01b9 (patch) | |
| tree | fb1320fc95bfac4828bc4424f23b202eb91d6807 /test-suite | |
| parent | 86041b8b5d6bc93d545554d1fdded70bf59eb880 (diff) | |
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
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/evars.v | 15 |
1 files changed, 13 insertions, 2 deletions
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 13814d9d8..f17fecc1e 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). + |