coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Tactic Notation and lists

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:

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.

Awesome! I am looking forward to that.

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, Pierre-Marie Pédrot, 04/12/2016