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 12:31:42 +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:fONAtRa2Y3ZbSG49SXTEgfj/LSx+4OfEezUN459isYplN5qZpcm7bnLW6fgltlLVR4KTs6sC0LqG9f25EjZbqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh7D0psSYOV4ArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Kq8/VPlTCCksG2Ez/szi8xfZHiWV4X5JaGIcmBdSH0Dm9hzwVJrrqWOus+N83CicMsn3VqwvcS6l5a1mUgPrkioNPTMj6yfRjpoj3+pgvBu9qkknkMbva4aPOa8mcw==
On 04/12/2016 11:33 AM, Pierre-Marie Pédrot wrote:
On 12/04/2016 11:24, Robbert Krebbers wrote:Awesome! I am looking forward to that.
I am wondering whether it is possible to manipulate such lists in Ltac.
Short answer: not yet, but I'm working on in in trunk.
May I put in two feature requests related to this:
* Being able to also manipulate intro_patterns in Ltac
* Being able to convert idents to (Coq) strings and vice versa.
- [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.