coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Digest for list coq-club (1/2)

From: 孙天宇 <stycyj AT bupt.edu.cn>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Digest for list coq-club (1/2)
Date: Wed, 12 Oct 2016 12:39:56 +0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=stycyj AT bupt.edu.cn; spf=Pass smtp.mailfrom=stycyj AT bupt.edu.cn; spf=None smtp.helo=postmaster AT mx1.bupt.edu.cn
Ironport-phdr: 9a23:cNuQpxDYL6aqWGNqosCTUyQJP3N1i/DPJgcQr6AfoPdwSP7/psbcNUDSrc9gkEXOFd2CrakV0ayK6uu/CCQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd+IyZjunL/js7ToICxwzAKnZr1zKBjk5S7wjeIxxbVYF6Aq1xHSqWFJcekFjUlhJFaUggqurpzopM0roGxsvKdr/MlZFK7+Yq4QTLpCDT1gPXp/rJngsgCGRg+S7FMdVH8Xm1xGGV6Wwgv9W8IJStOy4vFhySKLP+X8UKgoHzmu8uFgTkm72288Kzcl/TSP2YRLh6VBrUf5qg==

Thanks.

On 10/12/2016 10:36, coq-club-request AT inria.fr wrote:

Table of contents:

1. Re: [Coq-Club] questions about using search command in coqtop ideslave - CJ
Bell <siegebell+coq AT gmail.com>
2. Re: [Coq-Club] questions about using search command in coqtop ideslave -
zjhsdtc <zjhsdtc AT gmail.com>
3. Re: [Coq-Club] questions about using search command in coqtop ideslave -
James Smith <jecs AT imperial.ac.uk>
4. Re: [Coq-Club] questions about using search command in coqtop ideslave - CJ
Bell <siegebell+coq AT gmail.com>
5. [Coq-Club] API: How to generate a sort type for the parameter of an
abstraction - Sylvain Boulmé <Sylvain.Boulme AT imag.fr>
6. Re: [Coq-Club] API: How to generate a sort type for the parameter of an
abstraction - Guillaume Melquiond <guillaume.melquiond AT inria.fr>
7. Re: [Coq-Club] API: How to generate a sort type for the parameter of an
abstraction - Jean-Francois Monin <jean-francois.monin AT imag.fr>
8. Re: [Coq-Club] API: How to generate a sort type for the parameter of an
abstraction - Sylvain Boulmé <Sylvain.Boulme AT imag.fr>
9. Re: [Coq-Club] API: How to generate a sort type for the parameter of an
abstraction - Matthieu Sozeau <mattam AT mattam.org>
10. Re: [Coq-Club] API: How to generate a sort type for the parameter of an
abstraction - Sylvain Boulmé <Sylvain.Boulme AT imag.fr>
11. [Coq-Club] missing (?) dependency in Makefiles - Matej Košík
<matej.kosik AT inria.fr>
12. [Coq-Club] Equality for inductive type containing list - Klaus Ostermann
<klaus.ostermann AT uni-tuebingen.de>
13. Re: [Coq-Club] Equality for inductive type containing list - Dominique
Larchey-Wendling <dominique.larchey-wendling AT loria.fr>
14. Re: [Coq-Club] Equality for inductive type containing list - Clément Pit--
Claudel <clement.pit AT gmail.com>
15. Re: [Coq-Club] Equality for inductive type containing list - Klaus
Ostermann <klaus.ostermann AT uni-tuebingen.de>
16. Re: [Coq-Club] Equality for inductive type containing list - Dominique
Larchey-Wendling <dominique.larchey-wendling AT loria.fr>
17. Re: [Coq-Club] Equality for inductive type containing list - Pierre-Marie
Pédrot <pierre-marie.pedrot AT inria.fr>
18. Re: [Coq-Club] Equality for inductive type containing list - Maxime Dénès
<mail AT maximedenes.fr>
19. Re: [Coq-Club] Equality for inductive type containing list - Pierre-Marie
Pédrot <pierre-marie.pedrot AT inria.fr>
20. Re: [Coq-Club] Equality for inductive type containing list - Pierre
Courtieu <pierre.courtieu AT gmail.com>
21. Re: [Coq-Club] Equality for inductive type containing list - Abhishek
Anand <abhishek.anand.iitg AT gmail.com>
22. Re: [Coq-Club] Equality for inductive type containing list - Dominique
Larchey-Wendling <dominique.larchey-wendling AT loria.fr>
23. Re: [Coq-Club] Equality for inductive type containing list - Jonathan
Leivent <jonikelee AT gmail.com>
24. Re: [Coq-Club] Equality for inductive type containing list - Pierre-Marie
Pédrot <pierre-marie.pedrot AT inria.fr>
25. Re: [Coq-Club] questions about using search command in coqtop ideslave -
James Smith <jecs AT imperial.ac.uk>

Re: [Coq-Club] Digest for list coq-club (1/2), 孙天宇, 10/12/2016