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 
  • From: Benjamin Pierce <bcpierce AT cis.upenn.edu>
  • To: coq-club AT inria.fr
  • Cc: pierre.courtieu AT gmail.com
  • Subject: Re: [Coq-Club] Software foundation for older versions of coq
  • Date: Mon, 21 Dec 2020 11:51:41 -0500
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=bcpierce AT cis.upenn.edu; spf=Pass smtp.mailfrom=bcpierce AT seas.upenn.edu; spf=None smtp.helo=postmaster AT mail-qv1-f50.google.com
  • Ironport-phdr: 9a23:ZuXQwR+jW13Q7/9uRHKM819IXTAuvvDOBiVQ1KB31+4cTK2v8tzYMVDF4r011RmVBNqdsaoewLaP+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxhKiTanf79+MAu6oQreu8ULnIBvNrs/xhzVr3VSZu9Y33loJVWdnxb94se/4ptu+DlOtvwi6sBNT7z0c7w3QrJEAjsmNXs15NDwuhnYUQSP/HocXX4InRdOHgPI8Qv1Xpb1siv9q+p9xCyXNtD4QLwoRTiv6bpgRRn1gykFKjE56nnahdB/g6xGoByupRJxzYHXboGbKvRwebjQfc8DRWpEQspRVzBND4G6YoASD+QBJ+FYr4zlqlYTsxS+AwusC/nqyj9JgH/9wLc00+U/HgHcwAMvAc8FvXPPo9rpLKcSUP66zLPUwjrddP5ZxTb96JPSfhA8ufGDQ7RwcczLxUYxCgzFk0ydpIr4NDyayuoDqXKU7/Z8Ve2xkW4nrRl8ryauy8oohIfEgp4Zxk3Y+Sh5xIs4OdO2RUpnbNOrE5ZdtTyWOot1T84iQGxlujo2x6MHtJO/fSUHx5UqyhzDZvGBboOG4QrjWf6PLTtkgH9pYrGyihao/US+1+HxUtO43VZWoiZdj9XAqnMA2wbc58SdVPdw8Vut1SyN2g3d7OxPPFo6mrDBK5E7x749jpoTvlrHHi/xgEj2ibWZdkQg+uSx8uTnfKjqqoaSN4J0lg3yKKsumsu4AeQ3NggBQXKX9vi71L3m5UH5QbNKgeMqkqTBrpzWOcAWqrS6DgJVyIov9QuzAjO83NkYgXULNFdFdwiGj4jtNVHOOvf4DfKnjlu3jDhr3/HGMaP7AprRMHfOi6zhcqhn5E5H0gYz0Mhf6IxSCrEHOv78RFL+tMHAAh8jLwO02/rnCMl61o4GRW2PBbaZPLrOvl+M++IgOPKBZJQVuTb4M/gq/eTijX4/mV8HfKmmx4EbaH6iHqcuH0LMan31x9wFDG0ivwwkTeWshkfRfyRUYiOYUqQ+7zQ6DsqeDIrZTY3l1LaKxCa2BJZbTmtHERaRCXruccOJV+paO3HaGdNojjFRDevpcIQmzxz77FarmYoiFfLd/2gjjbym0dF04+PJkhRrq25vAs2GlXyVQmdy2G4EWm1vhf0tkQlG0l6GlJNArblYGNhUva4bVw47MdvF0bU/BY2qHA3GediNRRCtRdD0WWhtHOJ0+McHZgNGI/vnlgrKhnf4CL4O0aGTCZoytK/QwiqpKg==

Maybe easiest just to give you access to the GitHub repo? What’s your handle?

- B

> On Dec 21, 2020, at 11:04 AM, Pierre Courtieu <pierre.courtieu AT gmail.com>
> wrote:
>
> 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