Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Tactic Notation and lists

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Tactic Notation and lists


Chronological Thread 
  • 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.



Archive powered by MHonArc 2.6.18.

Top of Page