Skip to Content.
Sympa Menu

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

Subject: Ssreflect Users Discussion List

List archive

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


Chronological Thread 
  • From: (Emilio Jesús Gallego Arias)
  • To: Kevin Buzzard <>
  • Cc: ssreflect mailing list <>
  • Subject: Re: [ssreflect] [Coq-Club] trouble setting up environment to analyse Feit-Thompson proof.
  • Date: Wed, 14 Jun 2017 16:05:31 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None ; spf=Neutral ; spf=None
  • Ironport-phdr: 9a23:75vcbxGOGb03oShHAnA1tZ1GYnF86YWxBRYc798ds5kLTJ7zpM2wAkXT6L1XgUPTWs2DsrQf2rWQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbQhFgDiwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VC+85Kl3VhDnlCYHNyY48G7JjMxwkLlbqw+lqxBm3oLYfJ2ZOP94c6jAf90VWHBBU95RWSJfH428aIUPAeQDMuhboYbyqEcBoACiBQWwHu7j1iNEi2X00KA8zu8vERvG3AslH98WrnvZt9r0OaQOXeyvy6nI1zrDZO5S1Tny7YjIcxQhofCLXbltdcTe11IvDxnejl6NqILqJTeV1uATvGiU6OprSP6ii3Qmqw5ruTijw8EhgZTHiIISz1DL7yR5wIAtKN23SU57fd6kEIZLuC2AK4R2RcYiTmd1syg50r0LoYO3cSwFxZg92RLTdvOKf5KV7h/jV+udOyp0iXxmdb6nhBu+7VKsxvD8W8Wu1FtHrTBJnsTDu30N0RHY99KJReFn/ki73DaCzwDT5f9AIUAzjafUN4IuzqcslpoOqUTMBCn2lFzsjK+RbEok/+mo6+LoYrn/vJCQLZF7igflMqQrgsyzG+o4MhIWU2ia/+SzyqHj8FXkTLhOgfA6iLfVvI3VKMgBu6K0AwxY3pw+5xuxDDqqyNEYkmMGLFJBdhKHlY/pO1TWLf/mFvq+jFehnCtxy/DBJL3hDY3BLmLfn7f5YbZ990lcxRIozdBE/ZJbFL8BIPbtVUDtqNzVFQQ5Mgyxw+b/EtpxzIIeWWSVAq+YKqzeq1GI5vh8a9WLMawYpjf7Y9I49eznl3NxzVwQY6ivm55RYm2qDP18L22WZHPthpEKFmJc7SQkS+m/hXWSAWYVYGy9F+IR4zA/CYXuL4rY1Jvlr7WF2Cq0GdV/fGFPERHfQj/Ta4yYVqJUO2qpKch7n2lBDOD5Rg==
  • Organization: X80 Heavy Industries
Hi Kevin,

[addressing this to the ssreflect list where the true experts on the
proof can see it]

Kevin Buzzard
<>
writes:

> I have the current ssreflect installed and it works fine for me in Coq
> 8.6 too. On reflection I think that my question is perhaps for the
> maintainers of the Feit-Thompson proof. It had not occurred to me that
> one might need to maintain a proof!

I am not sure if you are referring to the proof in the old directory,
but note that the proof is maintained (and works for me) in the github
repository I pointed to:

https://github.com/math-comp/math-comp/blob/master/mathcomp/odd_order/stripped_odd_order_theorem.v

That is to say, I think that if you use Coq 8.6 you should not rely on
the original published file.

E.

Archive powered by MHonArc 2.6.18.

Top of Page