Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Software foundation for older versions of coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Software foundation for older versions of coq


Chronological Thread 
    < Chronological >      < Thread >
  • From: Pierre Courtieu <pierre.courtieu AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Software foundation for older versions of coq
  • Date: Mon, 21 Dec 2020 17:04:00 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f43.google.com
  • Ironport-phdr: 9a23:mYkNph+A+KiDlP9uRHKM819IXTAuvvDOBiVQ1KB32+scTK2v8tzYMVDF4r011RmVBNqdsaoewLaP+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxhKiTanf79+MAu6oQreu8ULnIBvNrs/xhzVr3VSZu9Y33loJVWdnxb94se/4ptu+DlOtvwi6sBNT7z0c7w3QrJEAjsmNXs15NDwuhnYUQSP/HocXX4InRdOHgPI8Qv1Xpb1siv9q+p9xCyXNtD4QLwoRTiv6bpgRQT2gykbKTE27GDXitRxjK1FphKhuwd/yJPQbI2MKfZyYr/RcdYcSGFcXMheSjZBD5uzYIsBDeUPPehWoYrgqVUQsRSwChKhBP/2yjJSmnP6wbE23uYnHArb3AIgBdUOsHHModvvNacdT/q1zLPWwj7ecf5W3ir96JLUchAgv/6MQK97fM3JyUkuCQzFlE+QppL/MzyJ0eQNrnKb7/ZhVe2xlm4qsA5xoj21ycctjonFnJ4aylfB9Shgxos+ONK3RlJhb9G+DJtQqz+VN5FwQs46XWxkpiY0x70btJKnYCUEx5QqygPDZvGGbYWF7B3uWumTLDtkhX9ofLyxiwiv/UWixOPxS8a63lZXoidYkdTBuXYA3AHQ5MifUvZx4Fut1DKV2w3Q6uxIO104mKvaJpI7zbM9mJweulnZECDsgkX5lqqWe10k+ue27+TnZa3rppqGOI91jgHyK6UumsuiDeghPAgDUGaW9f6z1L3k+k35T7FKgeMsnqbFt5DaINwXpq+/AwBLzoYu8wizAyui3dgCnnQKLEhJdA+GgoXoIV3DL/71Ae+6g1u2kTdrw/7GPqfmApXINnXDiLbhcqhn605G1gU/18xQ55VJCrEbPPLzW1H+tMHDAx82Ngy72efnCNFn2owCXmKPB7eVMLnOvl+Q+uIvP+6MaZcJtzb6Mvgp/uLhjXskmVAGZqSpxpsWaHWgHvt8OUmZYHzsgs0AEWgQpAY+Qvbq2xW+Vmt4YG/6dKYh7HlvA4W/SIzHW4qFgbqb3S79EIcANU5cDVXZKXblbZ+JE9wLdTiOI8J82mgcVLW7UYJn3hazrhP7xqdPIe/d+ylevpXmgosmr9bPnA0/oGQnR/+W1HuAGiQtxjtRG20GmZtnqEk48W+tlLBiiqUBR9NW7vJNFAw9MMyElr0oO5XJQgvEO+yxZhOjS9SiDys2S4tokdALakd5Xd6li0Kahnf4M/ouj7WOQacM3Ofc0nz2fZsvzn/H0OwgiABjTJcUc2KhgaF7+k7YAIuby0g=
Hi Benjamin!
Actually I need lf and plf. lf failed but was easy to fix (Removing
Declare Scope), but plf failed more heavily (custom syntax not
supported ni the "where" clause it seems)
Best regards,
P.

Le lun. 21 déc. 2020 à 17:02, Benjamin Pierce <bcpierce AT cis.upenn.edu> a
écrit :
>
> Hi Pierre,
>
> Do you need just the first volume? This version is advertised to work with
> 8.8, so 8.9 might be fine.
>
> Otherwise I can give you access to the developer git repo and you can find
> what you need there.
>
> - B
>
>
> > On Dec 21, 2020, at 10:03 AM, Pierre Courtieu <pierre.courtieu AT gmail.com>
> > wrote:
> >
> > Hi, I post this question here, since I didn't find a more dedicated
> > channel. Please feel free to point me to a more appropriate one.
> >
> > For technical reasons I need a version of software foundation that
> > would compile with coq-8.9. What is the standard way to obtain it
> > please?
> >
> > Best regards,
> > Pierre
>

Archive powered by MHonArc 2.6.19+.

Top of Page