The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 07/03/2016 20:20, Beta Ziliani wrote:
> Hi all,
> 
> Say I have a plugin with a procedure "f" that processes a constr_expr,
> and I want to write a tactic for it. I can't write the following:
> 
> TACTIC EXTEND myf
>   | [ "myf" constr_expr(c) ] -> [ f c ]
>  
> Is there an argument for a constr_expr? Or should I change "f" to get an
> object of a distinct type? f uses Proofview, and the idea is to
> interpret c in the evarmap provided by the proofview.

If I read between the lines, what you want is not a constr_expr but
rather a glob_constr. If that is true, you can probably rely on the
"uconstr" argument to do what you want.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature