Stream: Coq devs & plugin devs

Topic: tauto plugin?

Gaëtan Gilbert (Jul 05 2021 at 11:43):

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

Pierre-Marie Pédrot (Jul 05 2021 at 12:21):

What's the reason for not having it separate?

Pierre-Marie Pédrot (Jul 05 2021 at 12:21):

Most other self-contained tactic plugins are separate.

Last updated: Feb 01 2023 at 15:04 UTC