coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Tactic Notation and lists
- Date: Tue, 12 Apr 2016 14:16:53 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mailinglists AT robbertkrebbers.nl; spf=None smtp.mailfrom=mailinglists AT robbertkrebbers.nl; spf=None smtp.helo=postmaster AT smtp1.science.ru.nl
- Ironport-phdr: 9a23:iZEYLB99h5STRf9uRHKM819IXTAuvvDOBiVQ1KB91uscTK2v8tzYMVDF4r011RmSDdWdtqsP17WempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+lSsiP1o/riKibwN76XUZhvHKFe7R8LRG7/036l/I9ps9cEJs30QbDuXBSeu5blitCLFOXmAvgtI/rpMYwu3cYh/V0/MlZFK7+Yq4QTLpCDT1gPXpmytfssEz5SgGF62EAGkYMnxBCDhLepEX/V5b1sy31sutmxDKyJ8r8R70uRTe44q1hRQXzziEDYW1quFrLg9B92foI6CmqoAZyltbZ
On 04/12/2016 02:14 PM, Pierre-Marie Pédrot wrote:
That's part of the global picture indeed.That sound truly great!
Can you give us some idea of the "global picture" that you are after?
- [Coq-Club] Tactic Notation and lists, Robbert Krebbers, 04/12/2016
- Re: [Coq-Club] Tactic Notation and lists, Pierre-Marie Pédrot, 04/12/2016
- Re: [Coq-Club] Tactic Notation and lists, Robbert Krebbers, 04/12/2016
- Re: [Coq-Club] Tactic Notation and lists, Pierre-Marie Pédrot, 04/12/2016
- Re: [Coq-Club] Tactic Notation and lists, Robbert Krebbers, 04/12/2016
- Re: [Coq-Club] Tactic Notation and lists, Pierre-Marie Pédrot, 04/12/2016
- Re: [Coq-Club] Tactic Notation and lists, Robbert Krebbers, 04/12/2016
- Re: [Coq-Club] Tactic Notation and lists, Pierre-Marie Pédrot, 04/12/2016
- Re: [Coq-Club] Tactic Notation and lists, Robbert Krebbers, 04/12/2016
- Re: [Coq-Club] Tactic Notation and lists, Pierre-Marie Pédrot, 04/12/2016
- Re: [Coq-Club] Tactic Notation and lists, Pierre-Marie Pédrot, 04/12/2016
Archive powered by MHonArc 2.6.18.