coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Getting Program's postcondition with a two-level dependent pattern matching?

From: Adam Koprowski <adam.koprowski AT gmail.com>
To: Matthieu Sozeau <mattam AT mattam.org>
Cc: Coq Club <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club] Getting Program's postcondition with a two-level dependent pattern matching?
Date: Sun, 28 Jun 2009 16:30:03 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; b=CrD+8xeC87TbmD5EFKdAn8K1d2PV/+o/RIv3BU1Zo0sBX03VWXLbBnBaxO8JZH8zHm +O4leKUYZKSaKPb/3zIZfEsypUkLvXuhe8HOQxktBeUFlV1G6JOnxHR41TDUhDLyz7co CjrHut7l7S77ToAKhRS7fXjRhndPmG3xWoPI4=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

It is fixed in the trunk now, enjoy !

� What can I say apart from: Matthieu, you rock! Big thanks man!
� Still, it's not so easy to get rid of me, I'm afraid ;). I'm still experimenting with Program and after your fix I found a problem with the catch-all pattern [_]; I filled a bug report: http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2130

�� Cheers,
�� Adam

--
=====================================================
Adam.Koprowski AT gmail.com, http://www.cs.ru.nl/~Adam.Koprowski
The difference between impossible and possible
lies in determination (Tommy Lasorda)
=====================================================

[Coq-Club] Getting Program's postcondition with a two-level dependent pattern matching?, Adam Koprowski
- Re: [Coq-Club] Getting Program's postcondition with a two-level dependent pattern matching?, Matthieu Sozeau
  - Re: [Coq-Club] Getting Program's postcondition with a two-level dependent pattern matching?, Adam Koprowski
    - Re: [Coq-Club] Getting Program's postcondition with a two-level dependent pattern matching?, Matthieu Sozeau
      - Re: [Coq-Club] Getting Program's postcondition with a two-level dependent pattern matching?, Adam Koprowski