As requested yesterday (during an Ltac2 breakout session at the 3rd iris workshop) I removed all unrolled tactic notations in ltac_tactics.v by using Ltac2/Ltac1 FFI which allows us to iterate over Ltac1 lists.
I had to introduce some auxiliary tactics in places where notation was re-used previously. This no longer works because
iIntros (xs) is not expanded to
iIntros (x1 .. xN). So every tactic notation that gets re-used in notation further down in the file needs to have an equivalent
Ltac tactic that can be called explicitly with all the arguments, especially lists such as
I have no interest in bikeshedding the exact names, locations, indentations, the code factoring, or anything like that. I would very much appreciate somebody taking over these parts. I will gladly answer questions about and help with anything Ltac2-related, of course.
Apart from bikeshedding issues there is really just one question remaining: which lists should be marked non-empty. I saw that
iClear for example does not demand an item in the list of coq idents so I wasn't sure if I should follow that example or not. For now I only marked the
iExists argument with the
ne_ prefix because that tactic definitely didn't accept an empty list before.