coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Tactic Notation and lists

From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Tactic Notation and lists
Date: Tue, 12 Apr 2016 11:33:32 +0200

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 it in trunk.

Cheers,
PMP

Attachment: signature.asc
Description: OpenPGP digital signature

[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