The Tactician, Interactive Tactic Learner and Prover for Coq

I wonder if some math vizard, have built a packed for this COQ plugin?

1 Like

I’m not aware of anyone who packaged this (but would love to be wrong!). I think the packaging is nontrivial for the reasons listed here

1 Like

Thanks for the link, its ecaped my search.