coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Vincent Siles <vincent.siles AT ens-lyon.org>
- To: Victor Porton <porton AT narod.ru>
- Cc: coq-club Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] A proposal for a new kind of hints in Coq
- Date: Wed, 9 Jan 2013 16:45:07 +0100
2013/1/9 Victor Porton <porton AT narod.ru>
>> Finally, if nobody is willing to implement this, I TREAT you that I will learn ML and do it myself!
>
> Oh, certainly I THREAT not treat. :-)
Or you could just start to learn Ltac
Cheers,
V.
Cheers,
V.
- [Coq-Club] A proposal for a new kind of hints in Coq, Victor Porton, 01/09/2013
- Re: [Coq-Club] A proposal for a new kind of hints in Coq, Victor Porton, 01/09/2013
- Re: [Coq-Club] A proposal for a new kind of hints in Coq, Victor Porton, 01/09/2013
- Re: [Coq-Club] A proposal for a new kind of hints in Coq, Vincent Siles, 01/09/2013
- Re: [Coq-Club] A proposal for a new kind of hints in Coq, Victor Porton, 01/09/2013
- Re: [Coq-Club] A proposal for a new kind of hints in Coq, Victor Porton, 01/09/2013
- Re: [Coq-Club] A proposal for a new kind of hints in Coq, Victor Porton, 01/09/2013
Archive powered by MHonArc 2.6.18.