Michael Soegtrop (Feb 15 2022 at 17:56): 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.?
Pierre-Marie Pédrot (Feb 15 2022 at 17:58):AFAIR it was implemented in master
Gaëtan Gilbert (Feb 15 2022 at 17:58):https://github.com/coq/coq/pull/15378
Pierre-Marie Pédrot (Feb 15 2022 at 17:58):probably not released yet though
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: Oct 12 2024 at 13:01 UTC