The Coq mailing list

[Beta Ziliani <bziliani AT famaf.unc.edu.ar>]

On Mon, Mar 7, 2016 at 7:28 PM, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

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.

Actually, I think what I need is an open_constr. Now the question is, what do I do with the sigmas? I get one from the goal, and one for each open_constr, which one should I use, or how should I combined them?

Many thanks!

Beta

 

PMP