Stream: Coq devs & plugin devs

Topic: `par:` documentation


view this post on Zulip Maxime Dénès (Jun 15 2020 at 17:19):

I could not find par: in the tactic index. Is it missing?

view this post on Zulip Gaëtan Gilbert (Jun 15 2020 at 17:20):

It's not a tactic, it's a selector https://coq.github.io/doc/master/refman/proof-engine/ltac.html#grammar-token-toplevel-selector

view this post on Zulip Maxime Dénès (Jun 15 2020 at 17:21):

and what about [> ... | ... ]? is it a tactic?

view this post on Zulip Maxime Dénès (Jun 15 2020 at 17:21):

or +?

view this post on Zulip Maxime Dénès (Jun 15 2020 at 17:22):

but ok, anyway I was looking for its documentation, so thanks for the pointer

view this post on Zulip Gaëtan Gilbert (Jun 15 2020 at 17:23):

[> bla] is ltac syntax https://coq.github.io/doc/master/refman/proof-engine/ltac.html#local-application-of-tactics

view this post on Zulip Gaëtan Gilbert (Jun 15 2020 at 17:24):

If by + you mean bullets they're commands https://coq.github.io/doc/master/refman/proof-engine/proof-handling.html#bullets

view this post on Zulip Maxime Dénès (Jun 15 2020 at 18:00):

and yet, they seem to be in the tactic index


Last updated: Oct 21 2021 at 20:02 UTC