I could not find
par: in the tactic index. Is it missing?
It's not a tactic, it's a selector https://coq.github.io/doc/master/refman/proof-engine/ltac.html#grammar-token-toplevel-selector
and what about
[> ... | ... ]? is it a tactic?
but ok, anyway I was looking for its documentation, so thanks for the pointer
[> bla] is ltac syntax https://coq.github.io/doc/master/refman/proof-engine/ltac.html#local-application-of-tactics
+ you mean bullets they're commands https://coq.github.io/doc/master/refman/proof-engine/proof-handling.html#bullets
and yet, they seem to be in the tactic index
Last updated: Dec 05 2023 at 12:01 UTC