The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

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"?  That happens, for example, if you do

let t := lazymatch goal with

             | [ |- True ] => constr:(1)

             | [ |- False ] => fail "Found False"

           end in

...

The closest I've managed to come is

let t := lazymatch goal with

             | [ |- True ] => constr:(1)

             | [ |- False ] => fail 1 "Found False"

           end in

let t' := match True with

             | _ => t

           end in

...

But I can't do this if I don't have access to the source of the tactic that fails in the lazymatch, and can't bump up the failure level from 0 to 1.

Thanks,

Jason