The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

Use Ltac2

Ltac2 foo arg := do something.

Ltac2 Set foo as old_foo := fun arg => old_foo arg || try something else.

Gaëtan Gilbert

On 23/12/2024 06:18, Jason Hu wrote:
> Hi all,
>
> Is there a way to update a tactic, so that it invokes the old version of 
> itself?
>
> Say,
>
> Ltac foo arg := do something
>
> Ltac foo arg ::= old_foo arg || try something else
>
> I've tried a few things to fill in old_foo, but all ended up getting into an 
> infinite loop.
>
> I would like to update the tactic, instead of shadowing it, because I would 
> also like to update the behaviors of other tactics that use foo.
>
> *Thanks,*
> *Jason Hu*
> *https://hustmphrrr.github.io/ <https://hustmphrrr.github.io/>*