The Coq mailing list

[Meven Lennon-Bertrand <mgapb2 AT cam.ac.uk>]

    Hi Jason,
    
    There's also smpl,
    for an extensible "try all these tactics". Although I guess you
    cannot pass it arguments, so it might be too naïve for what you want
    to do…
    
    Best,
Meven LENNON-BERTRAND
Postdoc – Computer Lab, University of Cambridge
www.meven.ac

On 23/12/2024 06:23, Gaëtan Gilbert wrote:

> (code
>       was slightly incorrect, foo neds to be declared mutable ie
>       
>       
>       Ltac2 mutable foo arg := do something.
>       
>       
>       )
>       
>       
>       Gaëtan Gilbert
>       
>       
>       On 23/12/2024 06:21, Gaëtan Gilbert wrote:
>       
> > 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/
> > >           
> > >         
> >         
> >       
>       
>