I think I asked this before, but can't find it any more: are there goal selectors in Ltac2, say
AFAIR it was implemented in master
probably not released yet though
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: Jun 01 2023 at 12:01 UTC