Stream: Coq devs & plugin devs

Topic: tauto plugin?

view this post on Zulip Gaëtan Gilbert (Jul 05 2021 at 11:43):

What's the reason for having tauto_plugin separate from ltac_plugin?

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 12:21):

What's the reason for not having it separate?

view this post on Zulip Pierre-Marie Pédrot (Jul 05 2021 at 12:21):

Most other self-contained tactic plugins are separate.

Last updated: Oct 21 2021 at 20:02 UTC