coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] trouble setting up environment to analyse Feit-Thompson proof.

From: e AT x80.org (Emilio Jesús Gallego Arias)
To: Kevin Buzzard <kevin.m.buzzard AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] trouble setting up environment to analyse Feit-Thompson proof.
Date: Wed, 14 Jun 2017 11:14:12 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Neutral smtp.mailfrom=e AT x80.org; spf=None smtp.helo=postmaster AT cc-tupan-roaming-a.ensmp.fr
Ironport-phdr: 9a23:OH4wpRXsMy2XvlzGyGDL3ktrAKPV8LGtZVwlr6E/grcLSJyIuqrYbBCAt8tkgFKBZ4jH8fUM07OQ6PG/HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjSwbLdwIRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KpwVhTmlDkIOCI48GHPi8x/kqRboA66pxdix4LYeZyZOOZicq/Ye94RWGhPUdtLVyFZAo2ycZYBD+0PPehWrYbzpFUBohSiCgS3GOPj1iVFimPq0aAg0eksFxzN0gw6H9IJtXTZtMv6ObwdUO220KXE1zLDb+lZ2Tzg7ITGfRUhofCIXbJxdsra1E0hGB3ejk2KsozuIjKb2f4Js2if8eVgWuWvgHM7pgFrozig3NwshozPi4kIxF7E8iB5z5w0Jd2+UEN7YNikEIFRty6ALYd2TNkiT3lnuCY71r0GuYO7czMQxJs7wB7fbvqKeJWL7BL7TOudPDN1iX1/dL6hmhq//lKsxvD8W8S3ylpGsyRIn9rUun0OyxDf8NWLR/tn8kql2juDzR3f5+5ELE0yiKHVMYQuwqQqmZoWqUnDHjH5mEHxjKKOakor5vGk6/j6YrX+vJCcMZZ4ihv5Mqs0n8y/AOI4MgcXU2eB4+izyrvj/Vb8QLVSlPE2nLPZvIjbJcQduKG5HxdY3psn5huwFTuqzskUkHYdIF5YeB+KjJLlN0zALf37Ffu/hk6jkDZvx/DIJL3hBZDNI2Ddn7r6crdw6FJQxBA0zdBF6JJYEqsBL+7rWk/tqNzYCQc0PBCzw+b+EdlyyoceWX+UDaKCK6PTsVqI5vo1LOWWZY8Vviz9K/k/6PL0g385gwxVQa78/pYJaXbwNOl0MUyDbTK4gdofEGFMu0w0Uf74gUeOeTFWbne2Gak742doJpihCNLObpD92PqGxijzXrBTZ2RHDRiuHGx6bM2rUvMIZS2VauZ7kzUfFOvyA7Q93A2j4Vepg4FsKfDZr2hB7cru
Organization: X80 Heavy Industries

Dear Kevin,

Kevin Buzzard
<kevin.m.buzzard AT gmail.com>
writes:

> Just to be clear -- I am using the proof files here
> https://gforge.inria.fr/projects/coqfinitgroup/

I think the updated files are at https://github.com/math-comp/math-comp,
they work fine for me in Coq 8.6.

E.

[Coq-Club] trouble setting up environment to analyse Feit-Thompson proof., Kevin Buzzard, 06/14/2017
- Re: [Coq-Club] trouble setting up environment to analyse Feit-Thompson proof., Kevin Buzzard, 06/14/2017
  - Re: [Coq-Club] trouble setting up environment to analyse Feit-Thompson proof., Emilio Jesús Gallego Arias, 06/14/2017
    - Re: [Coq-Club] trouble setting up environment to analyse Feit-Thompson proof., Kevin Buzzard, 06/14/2017