coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Difference between uconstr and open_constr

From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Difference between uconstr and open_constr
Date: Wed, 27 Jul 2016 08:36:30 +0200

On 27/07/2016 00:31, Jonathan Leivent wrote:
> 3. there is a "uconstr:(..)" form for Ltac, but no corresponding one for
> open_constr (although one can somewhat get around this via a Tactic
> Notation).

Note that from 8.6 there is indeed an open_constr:(...) scope as a
proper Ltac argument.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] Difference between uconstr and open_constr, Robbert Krebbers, 07/27/2016
- Re: [Coq-Club] Difference between uconstr and open_constr, Jonathan Leivent, 07/27/2016
  - Re: [Coq-Club] Difference between uconstr and open_constr, Jonathan Leivent, 07/27/2016
    - [Coq-Club] Shadowing binders abusively renamed?, Yannick, 07/27/2016
      - Re: [Coq-Club] Shadowing binders abusively renamed?, Jonathan Leivent, 07/27/2016
        
        Re: [Coq-Club] Shadowing binders abusively renamed?, Yannick, 07/27/2016
        
        Re: [Coq-Club] Shadowing binders abusively renamed?, Jonathan Leivent, 07/27/2016
  - Re: [Coq-Club] Difference between uconstr and open_constr, Pierre-Marie Pédrot, 07/27/2016