Stream: Ltac2

Topic: Goal selectors


view this post on Zulip Michael Soegtrop (Feb 15 2022 at 17:56):

I think I asked this before, but can't find it any more: are there goal selectors in Ltac2, say 2,3: reflexivity.?

view this post on Zulip Pierre-Marie Pédrot (Feb 15 2022 at 17:58):

AFAIR it was implemented in master

view this post on Zulip Gaëtan Gilbert (Feb 15 2022 at 17:58):

https://github.com/coq/coq/pull/15378

view this post on Zulip Pierre-Marie Pédrot (Feb 15 2022 at 17:58):

probably not released yet though

view this post on Zulip Michael Soegtrop (Feb 15 2022 at 18:01):

Thanks! Btw.: up to now I hardly used Ltac2 in proof mode - I used it mostly for automation and kept proofs and automation separate, but I now started to use it for proof mode as well and it is quite smooth - sometimes I work with Ltac2 for an hour and don't even notice until I do a lia or so.


Last updated: Jan 31 2023 at 10:01 UTC