The Coq mailing list

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

On 01/08/2014 17:06, Jason Gross wrote:
> Is there any way to run a tactic to get a constr?  That is, say I have a
> tac [t] which, when run, either returns a [constr], or does [fail
> <message>].  Is there any way to, in the enclosing tactic, say "run u on
> the constr returned by t if it returns a constr, and otherwise fail with
> the same message as t"?

The usual trick to do this is to use a CPS version of the tactic:
instead of returning the constr, you pass it to a continuation k. In
your case, you get something along the lines of:

let t k := lazymatch goal with
             | [ |- True ] => let ans := constr:(1) in k ans
             | [ |- False ] => fail "Found False"
           end in ...

There are some uses of this trick in the standard library, for instance
in the ring tactic if I remember well. Yet, if you don't have access to
the body of the tactic, I do not know if this is doable at all...

PMP

Attachment: signature.asc
Description: OpenPGP digital signature