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 14:14:06 +0200

On 12/04/2016 12:31, Robbert Krebbers wrote:
> 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.

That's part of the global picture indeed.

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